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

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

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


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




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

Моделирование и анализ информационных систем, 2013, том 20, номер 6, страницы 52–63 (Mi mais342)  
Автоматическая верификация C-программ на основе смешанной аксиоматической семантики

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

a Институт систем информатики им. А. П. Ершова СО РАН, 630090, Россия, г. Новосибирск, проспект Лаврентьева, 6
b Новосибирский государственный университет, 630090, г. Новосибирск, ул. Пирогова, д. 2
PDF полного текста (571 kB)
Список литературы:
PDF
HTML
Аннотация: Развитие проекта C-light привело к применению новых формализмов и реализации методов, которые облегчают процесс верификации С-программ. Смешанная аксиоматическая семантика предлагает выбор между упрощенными и общими правилами вывода условий корректности (УК) в зависимости от программных объектов и их свойств. Инфраструктура LLVM значительно упрощает реализацию анализатора и транслятора C-light программ. Метод семантических меток, предложенный ранее, теперь может быть безопасно использован в условиях корректности при их доказательстве. Рассмотрен пример из соревнования по верификации, иллюстрирующий применение нашей системы.
Ключевые слова: верификация, операционная семантика, аксиоматическая семантика, язык C, язык C-light, язык C-kernel, частичная корректность, ACSL, LLVM, Simplify.
Поступила в редакцию: 10.11.2013
Тип публикации: Статья
УДК: 519.681.3
Образец цитирования: И. В. Марьясов, В. А. Непомнящий, А. В. Промский, Д. А. Кондратьев, “Автоматическая верификация 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}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/mais342
  • https://www.mathnet.ru/rus/mais/v20/i6/p52
    • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    		Моделирование и анализ информационных систем
    Статистика просмотров:
    Страница аннотации:299
    PDF полного текста:249
    Список литературы:42
     
      Обратная связь:
    		  Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024