Формальная верификация — это процесс доказательства того, что некоторая программа выполняет все требования, записанные в ее формальной спецификации. В результате освоения этого курса слушатель сможет записывать требования к Си-программам на языке формальной спецификации 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