Формальные модели и верификация свойств программ с использованием предметно-ориентированных языков

Кривчиков Максим Александрович (Механико-математический факультет и НИИ механики МГУ имени М.В. Ломоносова). Начало семинара - 24 декабря 2014 г.

В рамках работы, результаты которой представлены в докладе, предлагается подход к верификации сложных, наукоемких программных комплексов. Его суть в том, чтобы описывать их покомпонентно с помощью языков, адекватно отражающих специфику предметной области (предметно-ориентированных языков), которые при этом имеют заданную формальную семантику. Для построения таких языков и их формальной семантики разработано промежуточное представление на основе λ-исчисления с зависимыми типами. Результаты тестовых испытаний демонстрируют программную реализуемость предлагаемого подхода и возможности его применения для описания фрагментов реально существующего и используемого на практике программного комплекса.

Семинар группы

Технологии программирования

Перейти к списку семинаров ИСП РАН