Читается в осеннем семестре на первом курсе магистратуры ВШЭ и втором курсе магистратуры МФТИ.
Преподаватель: к.ф.-м.н. Камкин Александр Сергеевич
Цели курса: познакомить студентов с методами формальной верификации программ, включая дедуктивные методы и методы проверки моделей (model checking); сформировать навыки, необходимые для практического применения инструментов верификации (Frama-C/AstraVer, SPIN).
Планируемые результаты обучения:
- знать базовые принципы формальной верификации программ;
- знать методы формализации семантики языков программирования;
- знать методы дедуктивной верификации программ;
- знать методы проверки моделей компьютерных систем;
- уметь описывать условия корректности программ в виде пред- и постусловий;
- уметь аналитически доказывать частичную и полную корректность программ;
- уметь строить формальные модели компьютерных систем;
- уметь описывать свойства реагирующих систем в виде формул темпоральной логики;
- владеть навыками спецификации и моделирования программ;
- владеть навыками аналитической верификации программ;
- владеть инструментами дедуктивной верификации программ (Frama-C/AstraVer);
- владеть инструментами проверки моделей компьютерных систем (SPIN).
Рассматриваемые темы:
- Введение в формальные методы верификации программ (общая схема формальной верификации, подходы к формальной верификации, методы формализация семантики языков программирования).
- Дедуктивная верификация программ (метод Флойда, инструменты Frama-C/AstraVer, автоматическое доказательство теорем, SAT- и SMT-решатели).
- Проверка моделей компьютерных систем (темпоральная логика LTL, инструмент SPIN, автоматы Бюхи и регулярные w-языки, символическая проверка моделей, двоичные решающие диаграммы).
- Тестирование на основе моделей (проверка поведения, генерация тестовых воздействий, критерии тестового покрытия)