Формальная верификация — это процесс доказательства того, что некоторая программа выполняет все требования, записанные в ее формальной спецификации. В результате освоения этого курса слушатель сможет записывать требования к Си-программам на языке формальной спецификации ACSL и верифицировать Си-программы небольшого и среднего размера методами дедуктивной (или, по-другому, аналитической) верификации при помощи инструментов AstraVer, Why3 и ряда современных солверов (Alt-Ergo, CVC4, Z3).

Лекции и семинары

  1. Блок-схемы, определение частичной и полной корректности (слайды) (упражнения)

  2. Метод индуктивных утверждений (слайды) (упражнения)

  3. Метод фундированных множеств (слайды) (упражнения)

  4. Методы Флойда для блок-схем с вызовами других блок-схем, рекурсия (слайды) (упражнения)

  5. Триггеры (слайды) (упражнения)

  6. Леммы, ghost-блок-схемы, auto-active verification (слайды) (упражнения)

  7. WhyML, автоматизация построения условий верификации (слайды) (упражнения)

  8. Добавление новых типов и функций. (слайды) (упражнения)

  9. Моделирование массивов (слайды) (упражнения)

  10. Моделирование памяти Си-программы (слайды) (упражнения)

  11. Фрейм функции. Язык спецификации ACSL (слайды) (упражнения)

  12. Инструмент AstraVer: модель памяти, статическое разрешение синонимии указателей (слайды) (упражнения)

  13. Моделирование Java-программ (слайды)

  14. Инструмент AstraVer: приведение типов указателей, noembed, итоги (слайды)

Практикум

В практикуме 5 заданий. В каждом обычно 3 подзадания. У заданий есть дедлайны. После дедлайна решения по заданию не принимаются. Плагиат приводит к обнулению баллов за задание.

Задания 1-3 – это упражнения к лекциям. Задания 4-5 – это реализация на языке Си, формальная спецификация и формальная верификация реалистичного примера кода.

Инструкция по установке инструментов для практикума

Инструкция по установке солвера CVC4 1.8 (автор - Анастасия Богатенкова)

Условие Дедлайн
Задание 1 10 марта
Задание 2 10 апреля
Задание 3 10 мая
Задание 4 10 мая
Задание 5 31 мая

Оценивание

Итоговая оценка выставляется на основе оценки за семестр и оценки за экзамен. Оценка за семестр выставляется на основе суммы баллов за задания практикума и за задания контрольных работ.

Баллы за практикум:

Задание Оценка
Задание 1 0-10 баллов
Задание 2 0-10 баллов
Задание 3 0-10 баллов
Задание 4 0-10 баллов
Задание 5 0-20 баллов

Каждая контрольная работа оценивается до 20 баллов.

Оценка за семестр:

Сумма баллов Оценка
80-100 5
60-79 4
40-59 3
0-39 2

Итоговая оценка:

Оценка Семестр 5 Семестр 4 Семестр 3 Семестр 2
Экзамен 5 5 5 4 3
Экзамен 4 5 4 4 3
Экзамен 3 4 3 3 3
Экзамен 2 3 2 2 2

Литература

  1. Корныхин Е., Петренко А., Хорошилов А. (2020) Дедуктивная верификация блок-схем
  2. Bobot, F., Filliâtre, J., Marché, C. et al. (2015) Let’s verify this with Why3. In: International Journal on Software Tools Technology Transfer 17, 709–727.
  3. Why3 Documentation, версия 0.88.2
  4. ACSL: ANSI/ISO C Specification Language
  5. Claude Marché, Yannick Moy (2018) The Jessie pluginfor Deductive Verification in Frama-C.
  6. Hubert T., Marche C. (2007) Separation analysis for deductive verification. In: Heap Analysis and Verification (HAV’07). Braga, Portugal : March, 2007, p.81-93.
  7. Mandrykin, M.U., Khoroshilov, A.V. (2015) High-level memory model with low-level pointer cast support for Jessie intermediate language. In: Programming and Computer Software, 41, 197–207.
  8. Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov (2018) Lemma Functions for Frama-C: C Programs as Proofs. In: 2018 Ivannikov ISPRAS Open Conference
  9. Blanchard A., Loulergue F., Kosmatov N. (2019) Towards Full Proof Automation in Frama-C Using Auto-active Verification. In: Badger J., Rozier K. (eds) NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science, vol 11460. Springer, Cham
  10. Becker N., Müller P., Summers A.J. (2019) The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations. In: Vojnar T., Zhang L. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2019. Lecture Notes in Computer Science, vol 11427. Springer, Cham