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

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

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


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




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

Труды института системного программирования РАН, 2017, том 29, выпуск 6, страницы 49–76
DOI: https://doi.org/10.15514/ISPRAS-2017-29(6)-3 (Mi tisp273) 		 
Эта публикация цитируется в 2 научных статьях (всего в 2 статьях)

Формальная верификация библиотечных функций ядра Linux

Д. В. Ефремовa, М. У. Мандрыкинb

a НИУ Высшая школа экономики
b Институт системного программирования им. В.П. Иванникова РАН
PDF полного текста (824 kB) Список цитирования (2)
Список литературы:
PDF
HTML
DOI: https://doi.org/10.15514/ISPRAS-2017-29(6)-3
Аннотация: В статье авторами рассматриваются результаты дедуктивной верификации набора из 26 библиотечных функций ядра ОС Linux с помощью стека инструментов AstraVer. В набор включены преимущественно функции, работающие с данными строкового типа. Целью верификации является доказательство свойств функциональной корректности. В статье рассматриваются аналогичные работы по верификации, сравниваются полученные результаты, рассматривается ряд проблем, с которыми сталкивались авторы предыдущих работ, в том числе проблемы, с которыми удалось справится в рамках данной работы и те, которые все ещё препятствуют успешной верификации. Также предлагается методология разработки спецификаций, примененная для рассматриваемого набора функций, которая включает некоторые шаблонные приёмы разработки спецификаций. Авторам удалось доказать полную корректность двадцати пяти функций. В статье приведены результаты доказательства полученных условий верификации каждой функции с помощью нескольких современных SMT-солверов.
Ключевые слова: статический анализ, формальная верификация, дедуктивная верификация, функции стандартной библиотеки.
Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 15-01-03024
Эта работа поддержана грантом РФФИ 15-01-03024.
Реферативные базы данных:
Тип публикации: Статья
Образец цитирования: Д. В. Ефремов, М. У. Мандрыкин, “Формальная верификация библиотечных функций ядра Linux”, Труды ИСП РАН, 29:6 (2017), 49–76
Цитирование в формате AMSBIB
\RBibitem{EfrMan17}
\by Д.~В.~Ефремов, М.~У.~Мандрыкин
\paper Формальная верификация библиотечных функций ядра Linux
\jour Труды ИСП РАН
\yr 2017
\vol 29
\issue 6
\pages 49--76
\mathnet{http://mi.mathnet.ru/tisp273}
\crossref{https://doi.org/10.15514/ISPRAS-2017-29(6)-3}
\elib{https://elibrary.ru/item.asp?id=32309066}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/tisp273
  • https://www.mathnet.ru/rus/tisp/v29/i6/p49
    • Эта публикация цитируется в следующих 2 статьяx:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    		Труды института системного программирования РАН
    Статистика просмотров:
    Страница аннотации:214
    PDF полного текста:137
    Список литературы:16
     
      Обратная связь:
    		  Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024