В рамках годового магистерского курса "Формальные методы в программной инженерии" в апреле 2021г. будет прочитан курс
"Язык WhyML и методы автоматического доказательства
в системе Why3".

Курс очный, примерно из пяти лекций.
Он будет проходить по вторникам, начало 16-20, ауд. 4117.
Первая лекция: 6 апреля.

Видео-лекции, презентации и другие материалы
будут доступны по адресу: https://persons.iis.nsk.su/files/persons/fmcfiles/why3cdecl.pdf

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

Why3 проще известных инструментов PVS и Coq.
При доказательстве в системе Why3 можно перейти в множество (~20) других систем автоматического доказательства, в том числе: Z3, Alt-Ergo, CVC4, Coq и др.
В последней версии инструмента Why3 произошли революционные изменения. Появилась полноценная интерактивная система команд управления доказательством.

Лектор: Шелехов Владимир Иванович.