Курс «Основы формальной верификации на Coq»

Главная страница « Информация « Спецкурсы «

Специальный курс «Основы формальной верификации на Coq» (Formal Verification Foundations in Coq)

Лекторы: доцент, кандидат физ.-мат. наук Кулямин Виктор Вячеславович, Черганов Тимофей Юрьевич.
Продолжительность: 36 часов лекции.
Семестр: весенний.
Аудитория: для студентов магистратуры. Сведения о записи на курс запросите по

Аннотация

Корректность разрабатываемых программ является одной из основных задач, стоящих перед каждым разработчиком и перед индустрией разработки программного обеспечения в целом. В курсе рассматривается один из подходов к решению этой задачи: использование строгих математических методов для формулирования и доказательства утверждений о программах. Все доказательства в курсе являются формальными и автоматически проверяются интерактивным доказателем теорем Coq.

Тематический план курса

1. Основы функционального программирования на Coq.
2. Зависимые типы и соответствие Карри–Ховарда.
3. Тактики для построения доказательств.
4. Основы логики на Coq.
5. Формальная верификация функциональных алгоритмов.
6. Семантика простого императивного языка программирования.
7. Логика Флойда–Хоара.
8. Сепарационная логика.
9. Формальная верификация программ на С.

Основная литература:
1) Benjamin C. Pierce et al. Software Foundations. https://softwarefoundations.cis.upenn.edu
2) The Coq Development Team. The Coq Reference Manual. https://coq.inria.fr/refman

Дополнительная литература:
3) Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, 2004. https://www.labri.fr/perso/casteran/CoqArt/index.html
4). Adam Chlipala. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013. http://adam.chlipala.net/cpdt
5) Andrew W. Appel et al. Program Logics for Certified Compilers. Cambridge University Press, 2014. https://vst.cs.princeton.edu/veric
6) Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. QED at Large: A Survey of Engineering of Formally Verified Software. Foundations and Trends in Programming Languages: Vol. 5: No. 2-3, pp 102-281, 2019. https://arxiv.org/abs/2003.06458

Предупреждение

Размещение на других ресурсах, а также коммерческое использование материалов, опубликованных в данном разделе, возможно только с разрешения авторов.

Обновлено: 9.II.2025