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

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

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



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






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


Модел. и анализ информ. систем, 2010, том 17, номер 3, страницы 5–28 (Mi mais20)  

Эта публикация цитируется в 5 научных статьях (всего в 5 статьях)

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

И. С. Ануреев, И. В. Марьясов, В. А. Непомнящий

Институт систем информатики им. А. П. Ершова СО РАН

Аннотация: Описывается смешанная аксиоматическая семантика языка C-kernel, являющегося ядром представительного подмножества языка C, названного C-light. Такая семантика позволяет во многих случаях упростить условия корректности верифицируемых программ. Данная семантика является основой разрабатываемого генератора условий корректности C-kernel-программ. Рассмотрен пример, иллюстрирующий применение правил вывода описанной семантики.

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

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

Образец цитирования: И. С. Ануреев, И. В. Марьясов, В. А. Непомнящий, “Верификация C-программ на основе смешанной аксиоматической семантики”, Модел. и анализ информ. систем, 17:3 (2010), 5–28

Цитирование в формате AMSBIB
\RBibitem{AnuMarNep10}
\by И.~С.~Ануреев, И.~В.~Марьясов, В.~А.~Непомнящий
\paper Верификация C-программ на основе смешанной аксиоматической семантики
\jour Модел. и анализ информ. систем
\yr 2010
\vol 17
\issue 3
\pages 5--28
\mathnet{http://mi.mathnet.ru/mais20}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais20
  • http://mi.mathnet.ru/rus/mais/v17/i3/p5

    ОТПРАВИТЬ: 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

    Эта публикация цитируется в следующих статьяx:
    1. В. А. Непомнящий, И. С. Ануреев, М. М. Атучин, И. В. Марьясов, А. А. Петров, А. В. Промский, “Верификация C-программ в мультиязыковой системе СПЕКТР”, Модел. и анализ информ. систем, 17:4 (2010), 88–100  mathnet
    2. М. М. Атучин, И. С. Ануреев, “Атрибутные аннотации и их применение в дедуктивной верификации C-программ”, Модел. и анализ информ. систем, 18:4 (2011), 21–33  mathnet
    3. М. С. Кропачева, А. И. Легалов, “Формальная верификация программ, написанных на функционально-потоковом языке параллельного программирования”, Модел. и анализ информ. систем, 19:5 (2012), 81–99  mathnet
    4. И. С. Ануреев, “Дедуктивная верификация телекоммуникационных систем, представленных на языке Си”, Модел. и анализ информ. систем, 19:6 (2012), 34–44  mathnet
    5. И. С. Ануреев, “На пути к технологии разработки операционной семантики компьютерных языков: унифицированный формат помеченных систем переходов”, Тр. СПИИРАН, 25 (2013), 255–276  mathnet
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:297
    Полный текст:88
    Литература:25
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020