Современные программы становятся всё более сложными, и ошибки в них могут стоить очень дорого — от уязвимостей в безопасности до сбоев в критически важных системах. Традиционное тестирование позволяет обнаружить лишь часть проблем, но никогда не даёт полной гарантии правильности.
Формальная верификация идёт дальше: она позволяет строго доказать корректность программы и быть уверенным в её работе на 100%.
Курс познакомит тебя с функциональным программированием, математическими доказательствами в системе Lean и их применением для верификации программ.
Пререквизиты
Кореквизиты: нет.
Для каких потоков доступен: без ограничений по курсу и программе обучения.
Лимит по количеству студентов: нет.
2 пары в неделю.
Нестеров Василий Андреевич, магистр в логике и формальных доказательствах, энтузиаст Lean theorem prover, работает в Numina — команде, занимающейся Neural theorem proving.
Соколов Павел Павлович, аспирант в теории языков программирования, энтузиаст формальных методов и функционального программирования с промышленным опытом программирования на Haskell в области ZK-SNARK.
Ивашкевич Евгений Васильевич, канд. физ.-мат. наук, ректор Центрального университета.
Курс состоит из трёх основных блоков и двух продвинутых.
Наша цель — научить тебя формально доказывать, что программа работает корректно, причём делать это так, чтобы компьютер мог верифицировать доказательство.