Telegram Group & Telegram Channel
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



group-telegram.com/metaprogramming/404
Create:
Last Update:

Нашел качественную диссертацию с обзором состояния дел в 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

BY Metaprogramming


Warning: Undefined variable $i in /var/www/group-telegram/post.php on line 260

Share with your friend now:
group-telegram.com/metaprogramming/404

View MORE
Open in Telegram


Telegram | DID YOU KNOW?

Date: |

As the war in Ukraine rages, the messaging app Telegram has emerged as the go-to place for unfiltered live war updates for both Ukrainian refugees and increasingly isolated Russians alike. Telegram, which does little policing of its content, has also became a hub for Russian propaganda and misinformation. Many pro-Kremlin channels have become popular, alongside accounts of journalists and other independent observers. Friday’s performance was part of a larger shift. For the week, the Dow, S&P 500 and Nasdaq fell 2%, 2.9%, and 3.5%, respectively. And while money initially moved into stocks in the morning, capital moved out of safe-haven assets. The price of the 10-year Treasury note fell Friday, sending its yield up to 2% from a March closing low of 1.73%. To that end, when files are actively downloading, a new icon now appears in the Search bar that users can tap to view and manage downloads, pause and resume all downloads or just individual items, and select one to increase its priority or view it in a chat.
from ye


Telegram Metaprogramming
FROM American