Лекторы: профессор В.А. Захаров, м.н.с. В.В. Подымов

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

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

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

Литература

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