Сборники трудов ИСП РАН


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

Ефремов Д.В. (ВШЭ, Москва, Россия)
Мандрыкин М.У. (ИСП РАН, Москва, Россия)

Аннотация

Целью верификации является доказательство свойств функциональной корректности. В статье рассматриваются аналогичные работы по верификации, сравниваются полученные результаты, рассматривается ряд проблем, с которыми сталкивались авторы предыдущих работ, в том числе проблемы, с которыми удалось справится в рамках данной работы и те, которые все ещё препятствуют успешной верификации. Также предлагается методология разработки спецификаций, примененная для рассматриваемого набора функций, которая включает некоторые шаблонные приёмы разработки спецификаций. Авторам удалось доказать полную корректность двадцати пяти функций. В статье приведены результаты доказательства полученных условий верификации каждой функции с помощью нескольких современных SMT-солверов.

Ключевые слова

статический анализ; формальная верификация; дедуктивная верификация; функции стандартной библиотеки

Издание

Труды Института системного программирования РАН, том 29, вып. 6, 2017, стр. 49-76.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(6)-3

Полный текст статьи в формате pdf Вернуться к содержанию тома