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

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

Логика Некорректности

October 12

Всем хорошо известна так называемая логика корректности Хоара, позволяющая формально доказать, что программа работает правильно. А что если мы захотим формально доказать, что в программе есть баг? Например, что программа упадет, если дать ей на вход очень большую строку, при этом не уточняя, какая именно это строка. Оказывается, процесс доказательства наличия бага в программе можно формализовать так же, как мы формализуем доказательство корректности с помощью логики Хоара, - используя "Логику Некорректности" В докладе мы поговорим про "Логику Некорректности": обсудим ее связь с логикой корректности Хоара, посмотрим на ее натуральный вывод и семантику, отловим пару багов и, наконец, рассмотрим, как она связана с Динамической Логикой и Relation Algebra.

Докладчик: Владимир Гладштейн

Материалы

Peter W. O’Hearn. 2020. Incorrectness Logic. Proc. ACM Program. Lang. 4, POPL, Article 10 (January 2020), 32 pages. https://doi.org/10.1145/3371078

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