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


Обзор подходов к моделированию памяти в инструментах статической верификации

М.У. Мандрыкин (ИСП РАН, Москва, Россия)
В.С. Мутилин (ИСП РАН, Москва, Россия)

Аннотация

В статье приведен обзор существующих подходов к моделированию памяти Си-программ в инструментах статической верификации. Обозначены основные проблемы, возникающие при разработке моделей памяти для языка Си. В обзоре рассматриваются две основные группы моделей памяти в зависимости от полноты поддержки областей памяти наперед не ограниченного размера. Среди моделей для ограниченных областей памяти рассматриваются модель, использующая результаты предварительного анализа алиасов, и модель на основе слабейших предусловий, использующая теорию неинтерпретируемых функций и логику первого порядка. Среди моделей для областей памяти наперед не ограниченного размера рассматривается типизированная модель, модель Бурсталла-Борната, модель с регионами и полная модель памяти для теории интерпретируемых множеств элементов списков, использованная ранее в инструменте дедуктивной верификации HAVOC.

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

статическая верификация; модели памяти; SMT-решатели

Издание

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

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

DOI: 10.15514/ISPRAS-2017-29(1)-12

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