Цель курса — познакомить слушателей с теоретическими и практическими аспектами такой области как верификация программного обеспечения, получить представление о том, как разрабатывать надёжное программное обеспечение (ПО).

Содержание дисциплины

Необходимость в формальной верификации (примеры и истории).
Метод хоара-флойда верификации программ.
Верификация параллельных вычислений.
Темпоральные логики ctl, ltl, ctl*.
Табличный алгоритм model checking для ctl.
Символьный model checking (obdd) с вычислением неподвижной точки.
Эффект справедливости. достоинства ltl. автоматы бюхи. трансляция ltl в бюхи.
Model checking для ltl. ddfs, promela, spin.
Редукция частичных порядков.
Абстракции и симуляция как средство упрощения модели. Модулярный model checking.
Модели реального времени. временные автоматы rltl. регионы. Model checking свойств реального времени.
Динамические логики и mu-исчисление. smt-проверка. статический анализ.

Литература

Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: ModelChecking. Изд-во МЦНМО, 2002. 417 c.
Ю.Г. Карпов. ModelChecking: верификация параллельных и распределенных программных систем. Изд-во БХВ-Петербург, 2010.
K. R. Apt, E.-R. Olderog. Verification of sequential and concurrent programs, Springer, 1997, 365 p.

Как пойти учиться на АСВК

Об учебе

Читаемые курсы

Требования к курсовой

Спецсеминары

Ознакомительный спецкурс

Вычислительные ресурсы

Оформление работ

Инструменты и сервисы

Публикации студентов

Программа магистратуры