Forwarded from Covalue
Нашел качественную диссертацию с обзором состояния дел в model checking на 2010й год:
Weißenbacher, [2010] "Program Analysis with Interpolants"
Вкратце идею проверки моделей можно описать так: мы хотим автоматически верифицировать программы, для этого мы аппроксимируем их моделями, то есть автоматами или системами переходов с конечным набором состояний, задаём спецификацию (обычно в какой-то разновидности пропозициональной темпоральной логики) и с помощью поисковых алгоритмов и эвристик исчерпывающе перебираем состояния модели, проверяя что для них всех спецификация верна.
Концептуально этот подход описывается теорией моделей (одним из двух основных разделов логики, второй - это теория доказательств, на которой основана теория типов и proof assistants). Интересно, что в моделчекинге примерно раз в декаду сменяется доминирующая парадигма, в целом его таймлайн выглядит примерно так:
* 1980е - зарождение самой идеи MC из работ Эдмунда Кларка по вычислению неподвижных точек для систем доказательств в предикат-трансформерах, использование BDD для компактификации состояний
* 1990е - дальнейшее ужатие состояний через partial order reduction, появление предикат-абстракции и CEGAR - методов автоматического конструирования моделей из набора assertions о программе
* 2000е - SAT/SMT-революция и уход от BDD, быстрая аппроксимация через интерполяцию Крейга
* 2010е - Аарон Брэдли изобретает семейство алгоритмов PDR (property directed reachability), где процесс построение инварианта чередуется и взаимодействут с построением контрпримера, взаимно усекая пространства поиска
* 2020е - ажиотаж вокруг техник из машинного обучения
Первые три декады и основные их идеи расписаны в первых двух с половиной главах диссертации (вторая половина третьей и четвертая главы более технические).
#automatedreasoning
Weißenbacher, [2010] "Program Analysis with Interpolants"
Вкратце идею проверки моделей можно описать так: мы хотим автоматически верифицировать программы, для этого мы аппроксимируем их моделями, то есть автоматами или системами переходов с конечным набором состояний, задаём спецификацию (обычно в какой-то разновидности пропозициональной темпоральной логики) и с помощью поисковых алгоритмов и эвристик исчерпывающе перебираем состояния модели, проверяя что для них всех спецификация верна.
Концептуально этот подход описывается теорией моделей (одним из двух основных разделов логики, второй - это теория доказательств, на которой основана теория типов и proof assistants). Интересно, что в моделчекинге примерно раз в декаду сменяется доминирующая парадигма, в целом его таймлайн выглядит примерно так:
* 1980е - зарождение самой идеи MC из работ Эдмунда Кларка по вычислению неподвижных точек для систем доказательств в предикат-трансформерах, использование BDD для компактификации состояний
* 1990е - дальнейшее ужатие состояний через partial order reduction, появление предикат-абстракции и CEGAR - методов автоматического конструирования моделей из набора assertions о программе
* 2000е - SAT/SMT-революция и уход от BDD, быстрая аппроксимация через интерполяцию Крейга
* 2010е - Аарон Брэдли изобретает семейство алгоритмов PDR (property directed reachability), где процесс построение инварианта чередуется и взаимодействут с построением контрпримера, взаимно усекая пространства поиска
* 2020е - ажиотаж вокруг техник из машинного обучения
Первые три декады и основные их идеи расписаны в первых двух с половиной главах диссертации (вторая половина третьей и четвертая главы более технические).
#automatedreasoning