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

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

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


Труды ИСП РАН:
Год:
Том:
Выпуск:
Страница:
Найти




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

Труды института системного программирования РАН, 2019, том 31, выпуск 5, страницы 37–62
DOI: https://doi.org/10.15514/ISPRAS-2019-31(5)-3 (Mi tisp452) 		 
Автоматическое доказательство корректности программ с динамической памятью

Ю. О. Костюковa, К. А. Батоевa, Д. А. Мордвиновba, М. П. Костицынa, А. В. Мисонижникa

a Санкт-Петербургский государственный университет
b JetBrains Research
PDF полного текста (1719 kB)
Список литературы:
PDF
HTML
DOI: https://doi.org/10.15514/ISPRAS-2019-31(5)-3
Аннотация: В данной работе изучаются теоретические основы автоматической модульной верификации императивных программ с динамической памятью. Вводится формализм композициональной символьной памяти, который используется для построения композиционального алгоритма, порождающего обобщённые кучи. Они являются термами исчисления символьных куч, которые описывают состояния произвольных циклических фрагментов программы. Выводимые в этом исчислении кучи соответствуют достижимым состояниям исходной программы. В работе также устанавливается соответствие между выводом в этом исчислении и исполнением функциональных программ второго порядка без эффектов.
Ключевые слова: формальная верификация, автоматическая верификация, символьное исполнение, анализ программ, динамическая память, композициональность, чистые функции.
Тип публикации: Статья
Образец цитирования: Ю. О. Костюков, К. А. Батоев, Д. А. Мордвинов, М. П. Костицын, А. В. Мисонижник, “Автоматическое доказательство корректности программ с динамической памятью”, Труды ИСП РАН, 31:5 (2019), 37–62
Цитирование в формате AMSBIB
\RBibitem{KosBatMor19}
\by Ю.~О.~Костюков, К.~А.~Батоев, Д.~А.~Мордвинов, М.~П.~Костицын, А.~В.~Мисонижник
\paper Автоматическое доказательство корректности программ с динамической памятью
\jour Труды ИСП РАН
\yr 2019
\vol 31
\issue 5
\pages 37--62
\mathnet{http://mi.mathnet.ru/tisp452}
\crossref{https://doi.org/10.15514/ISPRAS-2019-31(5)-3}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/tisp452
  • https://www.mathnet.ru/rus/tisp/v31/i5/p37
    • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    		Труды института системного программирования РАН
    Статистика просмотров:
    Страница аннотации:115
    PDF полного текста:20
    Список литературы:18
     
      Обратная связь:
    		  Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024