УДК: 004.423.4

Формальные модели программ и языков программирования. Часть 2. Современное состояние исследований

В. А. Васенин, д-р физ.-мат. наук, зав. лаб., e-mail: vasenin@msu.ru, М. А. Кривчиков, науч. сотр., e-mail: maxim.krivchikov@gmail.com, НИИ механики МГУ имени М. В. Ломоносова, г. Москва

Настоящая статья продолжает опубликованные в № 5, 2015, результаты исследований. На основе анализа публикаций зарубежных и российских авторов с 1990-х годов по настоящее время дана оценка современному состоянию исследований в области формальной верификации программ. Основное внимание при этом уделено подходу к верификации на основе языков программирования с зависимыми типами. Рассмотрены также результаты и на других, смежных направлениях исследований. Обозначены потенциально перспективные, по мнению авторов, направления дальнейших исследований в этой области.

Ключевые слова: формальная верификация, языки программирования, предметно-ориентированные языки, формальная семантика программ, программная инженерия, библиография

Стр. 24–33