Исследовательская группа

Лаборатория языковых инструментов

О представимости инвариантов программ с алгебраическими типами данных

October 26

Со времён появления логики Хоара принято выражать свойства и сертификаты корректности программ на языках первого порядка. Современные методы автоматического вывода индуктивных инвариантов программ ориентированы на представление инвариантов также в логике первого порядка. Хотя такие представления очень выразительны для некоторых теорий (LIA, LRA BV, теория массивов), они не позволяют выразить многие интересные свойства программ над алгебраическими типами данных (АТД).

В докладе будут рассмотрены три различных подхода к представлению индуктивных инвариантов программ над АТД: формулами первого порядка, древовидными автоматами и формулами первого порядка с ограничениями на размер. Мы сравним их выразительную мощность и увидим на простых примерах, что очень часто современные инструменты вывода инвариантов не будут завершаться по причине непредставимости инварианта в языке. Также мы рассмотрим, как автоматически выводить регулярные инварианты программ над АТД с помощью инструментов поиска конечных моделей. Будет представлено сравнение эффективности вывода регулярных инвариантов через построение конечных моделей с современными Хорн-решателями.

Докладчик: Юрий Костюков

Материалы

1). Zhang T., Sipma H. B., Manna Z. Decision procedures for recursive data structures with integer constraints //International Joint Conference on Automated Reasoning. – Springer, Berlin, Heidelberg, 2004. – С. 152-167.

2). Reynolds A. J. Finite model finding in satisfiability modulo theories. – 2013.

Семинар пройдет онлайн 26 октября в 17:30, ссылка Google meet: https://meet.google.com/myu-dhmz-gvu