Информация о статье

2017 г., Том 22, Специальный выпуск, с.44-59

Кондратьев Д.А.

Расширение системы C-light символическим методом верификации финитных итераций

При разработке в ИСИ СО РАН дедуктивной системы C-light встала задача создания специализированных версий генераторов условий корректности (УК). Для ее решения использована концепция метагенерации УК.

Концепция семантических меток позволяет использовать саму процедуру генерации УК для построения их объяснений. Система C-light простым образом дополняется таким расширением с помощью метода метагенерации.

Проблема элиминации инвариантов циклов является алгоритмически разрешимой для циклов специального вида с помощью символического метода верификации финитных итераций. Для таких циклов применяются специальные правила вывода, позволяющие отказаться от использования инварианта цикла. Метод метагенерации позволил удобным образом расширить систему C-light такими правилами.

[полный текст]
Ключевые слова: верификация, метод метагенерации, символический метод верификации финитных итераций, условие корректности, метод семантической разметки

Библиографическая ссылка:
Кондратьев Д.А. Расширение системы C-light символическим методом верификации финитных итераций // Вычислительные технологии. 2017. Т. 22. XVII Всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям. С. 44-59
Главная| Цели| Редколлегия| Содержание| Поиск| Подписка| Правила| Контакты
ISSN 1560-7534
© 2024 ФИЦ ИВТ, Новосибирск