Формальная верификация — это процесс доказательства того, что некоторая программа выполняет все требования, записанные в ее формальной спецификации. В результате освоения этого курса слушатель сможет записывать требования к Си-программам на языке формальной спецификации ACSL и верифицировать Си-программы небольшого и среднего размера методами дедуктивной (или, по-другому, аналитической) верификации при помощи инструментов AstraVer, Why3 и ряда современных солверов (Alt-Ergo, CVC4, Z3).
Лекции и семинары
-
Блок-схемы, определение частичной и полной корректности (слайды) (упражнения)
-
Метод индуктивных утверждений (слайды) (упражнения)
-
Метод фундированных множеств (слайды) (упражнения)
-
Методы Флойда для блок-схем с вызовами других блок-схем, рекурсия (слайды) (упражнения)
-
Триггеры (слайды) (упражнения)
-
Леммы, ghost-блок-схемы, auto-active verification (слайды) (упражнения)
-
WhyML, автоматизация построения условий верификации (слайды) (упражнения)
-
Добавление новых типов и функций. (слайды) (упражнения)
-
Моделирование массивов (слайды) (упражнения)
-
Моделирование памяти Си-программы (слайды) (упражнения)
-
Фрейм функции. Язык спецификации ACSL (слайды) (упражнения)
-
Инструмент AstraVer: модель памяти, статическое разрешение синонимии указателей (слайды) (упражнения)
-
Моделирование Java-программ (слайды)
-
Инструмент 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 |
Литература
- Корныхин Е., Петренко А., Хорошилов А. (2020) Дедуктивная верификация блок-схем
- 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.
- Why3 Documentation, версия 0.88.2
- ACSL: ANSI/ISO C Specification Language
- Claude Marché, Yannick Moy (2018) The Jessie pluginfor Deductive Verification in Frama-C.
- Hubert T., Marche C. (2007) Separation analysis for deductive verification. In: Heap Analysis and Verification (HAV’07). Braga, Portugal : March, 2007, p.81-93.
- 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.
- Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov (2018) Lemma Functions for Frama-C: C Programs as Proofs. In: 2018 Ivannikov ISPRAS Open Conference
- 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
- 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