Разработка унифицированного интерфейса к решателям условий корректности

Abstract

Объект исследования: предметно-ориентированные системы переходов (унифицированный формализм для описания средств дедуктивной верификации программ) и язык выполнимых спецификаций предметно-ориентированных систем переходов Atoment, разработанные в лаборатории теоретического программирования ИСИ СО РАН. Цель исследования: разработка библиотеки, реализующей унифицированный интерфейс к решателям условий корректности и поддерживающей ввод условий корректности в виде элементов языка Atoment. Актуальность: большая часть существующих систем верификации интегрирована с одним или двумя решателями условий корректности. Поэтому создание унифицированного интерфейса к решателям условий корректности, является актуальной задачей. Метод исследования Исследовательская часть работы: изучение области дедуктивной верификации, изучение предметно-ориентированных систем и языка Atoment, разработка языка обработки условий корректности VCHL (Verification Condition Handling Language), проектирование библиотеки, построение операционной семантики языка VCHL. Реализационная часть работы: разработка библиотеки, реализующей интерфейс для решателей условий корректности, разработка тестов для проверки корректности работы библиотеки. Полученные результаты: библиотека, реализующая интерфейс к решателям условий корректности на предметно-ориентированном языке Atoment; предметно-ориентированный язык обработки условий корректности. Область применения: дедуктивная верификация программ, автоматическое и полуавтоматическое доказательство теорем.