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: |

Founder Pavel Durov says tech is meant to set you free "He has to start being more proactive and to find a real solution to this situation, not stay in standby without interfering. It's a very irresponsible position from the owner of Telegram," she said. Telegram has become more interventionist over time, and has steadily increased its efforts to shut down these accounts. But this has also meant that the company has also engaged with lawmakers more generally, although it maintains that it doesn’t do so willingly. For instance, in September 2021, Telegram reportedly blocked a chat bot in support of (Putin critic) Alexei Navalny during Russia’s most recent parliamentary elections. Pavel Durov was quoted at the time saying that the company was obliged to follow a “legitimate” law of the land. He added that as Apple and Google both follow the law, to violate it would give both platforms a reason to boot the messenger from its stores. Now safely in France with his spouse and three of his children, Kliuchnikov scrolls through Telegram to learn about the devastation happening in his home country. The original Telegram channel has expanded into a web of accounts for different locations, including specific pages made for individual Russian cities. There's also an English-language website, which states it is owned by the people who run the Telegram channels.
from sa


Telegram Metaprogramming
FROM American