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