Методы верификации программ

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

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

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

  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.

© 2011-2018 Лаборатория Вычислительных комплексов факультета ВМК МГУ