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

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

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



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






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


Модел. и анализ информ. систем, 2017, том 24, номер 6, страницы 743–754 (Mi mais597)  

Invariant elimination of definite iterations over arrays in C programs verification

[Элиминация инвариантов финитных итераций над массивами при верификации Си программ]

I. V. Maryasov, V. A. Nepomniaschy, D. A. Kondratyev

A. P. Ershov Institute of Informatics Systems SB RAS, 6 Akademik Lavrentyev av., Novosibirsk 630090, Russia

Аннотация: Данная работа представляет дальнейшее развитие метода верификации финитной итерации [7]. Он расширяет метод смешанной аксиоматической семантики [1], предложенный для верификации C-light программ. Это расширение включает метод верификации для финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию, выражающую действие тела цикла. Данное правило было реализовано в генераторе условий корректности, являющемся частью нашей системы верификации C-light программ. Для доказательства порождённых условий корректности применяется метод математической индукции, вызывающий сложности у SMT-решателей. В нашей системе верификации на стадии доказательства используется SMT-решатель CVC4. Для преодоления упомянутой трудности применяется стратегия переписывания условий корректности. Для доказательства условий корректности предложен метод, основанный на расширении теории новыми теоремами. Рассмотрен пример, иллюстрирующий применение данных методов. Статья публикуется в авторской редакции.

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

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


DOI: https://doi.org/10.18255/1818-1015-2017-6-743-754

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

Реферативные базы данных:

Тип публикации: Статья
УДК: 004.052.42
Поступила в редакцию: 08.09.2017
Язык публикации: английский

Образец цитирования: I. V. Maryasov, V. A. Nepomniaschy, D. A. Kondratyev, “Invariant elimination of definite iterations over arrays in C programs verification”, Модел. и анализ информ. систем, 24:6 (2017), 743–754

Цитирование в формате AMSBIB
\RBibitem{MarNepKon17}
\by I.~V.~Maryasov, V.~A.~Nepomniaschy, D.~A.~Kondratyev
\paper Invariant elimination of definite iterations over arrays in C programs verification
\jour Модел. и анализ информ. систем
\yr 2017
\vol 24
\issue 6
\pages 743--754
\mathnet{http://mi.mathnet.ru/mais597}
\crossref{https://doi.org/10.18255/1818-1015-2017-6-743-754}
\elib{http://elibrary.ru/item.asp?id=30730613}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais597
  • http://mi.mathnet.ru/rus/mais/v24/i6/p743

    ОТПРАВИТЬ: 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
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:107
    Полный текст:59
    Литература:14
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019