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


Моделирование памяти с использованием неинтерпретируемых функций в предикатных абстракциях

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

Аннотация

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

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

модель памяти, предикатная абстракция, метод уточнения абстракций по контрпримеру

Издание

Труды Института системного программирования РАН, том 27, вып. 5, 2015, стр. 117-142.

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

DOI: 10.15514/ISPRAS-2015-27(5)-7

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