Четверг, 11 марта, 18:30. "Введение в формальную верификацию программ" (А. Трунов)

[Alexander V. Smal]

Добрый день!

В следующий четверг 11 марта начнётся курс Антона Трунова (Zilliqa
Research) "Введение в формальную верификацию программ".
Занятия будут проходить по четвергам в 18:30.
https://compsciclub.ru/courses/formalverification/2021-spring/

Все лекции будут читаться через zoom. Ссылка для подключения будет
опубликована в новостях курса - её получат те, кто запишется на курс.
Участие в лекциях бесплатно и открыто для всех.

Аннотация курса:

Формальная верификация программ — это набор парадигм, техник и
инструментов, гарантирующих с той или иной степенью надёжности
корректность программ. Думаю многие согласятся, что есть области ИТ, в
которых корректность заслуживает самого пристального внимания:
прошивки бортовых компьютеров самолетов, автомобилей,
кардиостимуляторов, софт атомных электростанций и др.

Формальная верификация — это большая область, которую невозможно
покрыть в одном курсе сколько-нибудь глубоко, поэтому нашей целью
будет система интерактивного доказательства теорем Coq
(https://coq.inria.fr), теория типов, лежащей в ее основе,
метапрограммирование в Coq и применение Coq к верификации
функциональных алгоритмов.

Саша



--
Alexander V. Smal
St. Petersburg Department of Steklov Mathematical Institute
27 Fontanka, St. Petersburg, 191023, Russia