RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2018, том 25, номер 5, страницы 491–505 (Mi mais644)  

Верификация программ

Автоматизация верификации C-программ с использованием символического метода элиминации инвариантов циклов

Д. А. Кондратьев, И. В. Марьясов, В. А. Непомнящий

Институт систем информатики им. А.П. Ершова СО РАН, пр. Академика Лаврентьева, 6, г. Новосибирск, 630090 Россия

Аннотация: При дедуктивной верификации программ, написанных на императивных языках программирования, особую сложность вызывает порождение и доказательство условий корректности, соответствующих циклам, поскольку каждый из них должен быть снабжён инвариантом, построение которого часто является нетривиальной задачей. Методы синтеза инвариантов циклов, как правило, носят эвристический характер, что затрудняет их применение. Альтернативой является символический метод элиминации инвариантов циклов, предложенный В.А. Непомнящим в 2005 году. Его идея состоит в представлении тела цикла в виде специальной операции замены при выполнении определённых ограничений. Такая операция в символической форме выражает действие цикла, что позволяет ввести в аксиоматическую семантику правило вывода для циклов, не использующее инварианты. В данной работе представлено дальнейшее развитие этого метода. Он расширяет метод смешанной аксиоматической семантики, предложенный для верификации C-light программ. Данное расширение включает в себя метод верификации итераций над изменяемыми массивами с возможным выходом из тела цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов циклов. Данное правило было реализовано в генераторе условий корректности, являющемся частью системы автоматизированной верификации C-light программ. Для проведения автоматического доказательства в используемой системе ACL2 были разработаны и реализованы два алгоритма: первый порождает операцию замены на языке системы ACL2, а второй генерирует вспомогательные леммы, позволяющие системе ACL2 успешно доказать получаемые условия корректности в автоматическом режиме. Применение вышеуказанных методов и алгоритмов проиллюстрировано примером.

Ключевые слова: Си-лайт, инварианты циклов, смешанная аксиоматическая семантика, финитная итерация, массивы, ACL2, спецификация, верификация, логика Хоара.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 17-01-00789_а
Автор частично поддержан грантом РФФИ № 17-01-00789.


DOI: https://doi.org/10.18255/1818-1015-491-505

Полный текст: PDF файл (583 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 004.052.42
Поступила в редакцию: 10.09.2018

Образец цитирования: Д. А. Кондратьев, И. В. Марьясов, В. А. Непомнящий, “Автоматизация верификации C-программ с использованием символического метода элиминации инвариантов циклов”, Модел. и анализ информ. систем, 25:5 (2018), 491–505

Цитирование в формате AMSBIB
\RBibitem{KonMarNep18}
\by Д.~А.~Кондратьев, И.~В.~Марьясов, В.~А.~Непомнящий
\paper Автоматизация верификации C-программ с использованием символического метода элиминации инвариантов циклов
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 5
\pages 491--505
\mathnet{http://mi.mathnet.ru/mais644}
\crossref{https://doi.org/10.18255/1818-1015-491-505}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais644
  • http://mi.mathnet.ru/rus/mais/v25/i5/p491

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:47
    Полный текст:20
    Литература:4
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019