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

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

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

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

В последней версии инструмента Why3 произошли революцонные изменения. Появилась полноценная система команд управления доказательством.
Why3 проще известных инструментов PVS и Coq.
А при сочетании интерактивного (через команды) и автоматического (вызовом нескольких мощных SMT-решателей) режимов Why3 становится мощнее PVS и Coq.

Это хороший шанс для математиков начать освоение инструментов автоматического доказательства теорем.
Следующее поколение инструментов станет эффективно применимым для профессиональных математиков.