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

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

Аннотация

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

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

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


Основная литература:
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

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

© Кафедра системного программирования ВМК МГУ.

Обновлено: 11.II.2026