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

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

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



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






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


Модел. и анализ информ. систем, 2013, том 20, номер 6, страницы 52–63 (Mi mais342)  

Автоматическая верификация C-программ на основе смешанной аксиоматической семантики

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

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

Аннотация: Развитие проекта C-light привело к применению новых формализмов и реализации методов, которые облегчают процесс верификации С-программ. Смешанная аксиоматическая семантика предлагает выбор между упрощенными и общими правилами вывода условий корректности (УК) в зависимости от программных объектов и их свойств. Инфраструктура LLVM значительно упрощает реализацию анализатора и транслятора C-light программ. Метод семантических меток, предложенный ранее, теперь может быть безопасно использован в условиях корректности при их доказательстве. Рассмотрен пример из соревнования по верификации, иллюстрирующий применение нашей системы.

Ключевые слова: верификация, операционная семантика, аксиоматическая семантика, язык C, язык C-light, язык C-kernel, частичная корректность, ACSL, LLVM, Simplify.

Полный текст: PDF файл (571 kB)
Список литературы: PDF файл   HTML файл
Тип публикации: Статья
УДК: 519.681.3
Поступила в редакцию: 10.11.2013

Образец цитирования: И. В. Марьясов, В. А. Непомнящий, А. В. Промский, Д. А. Кондратьев, “Автоматическая верификация C-программ на основе смешанной аксиоматической семантики”, Модел. и анализ информ. систем, 20:6 (2013), 52–63

Цитирование в формате AMSBIB
\RBibitem{MarNepPro13}
\by И.~В.~Марьясов, В.~А.~Непомнящий, А.~В.~Промский, Д.~А.~Кондратьев
\paper Автоматическая верификация C-программ на основе смешанной аксиоматической семантики
\jour Модел. и анализ информ. систем
\yr 2013
\vol 20
\issue 6
\pages 52--63
\mathnet{http://mi.mathnet.ru/mais342}


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

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