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


Метод моделирования памяти в предикатных абстракциях с разделением на непересекающиеся области

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

Аннотация

Верификация программного обеспечения — вид деятельности, направленный на контроль качества программного обеспечения и обнаружения ошибок в нем. Статическая верификация - это один из способов верификации, который производится без выполнения исходного кода программы. Для статической верификации используется специальное программное обеспечение: инструменты статической верификации, которые часто работают с исходным кодом программы. Одним из таких инструментов является инструмент под названием CPAchecker. Проблема его текущей модели памяти заключается в том, что при встрече функции, возвращающей указатель на область памяти, у которой отсутствует тело, в процессе верификации о ее возвращаемом значении могут быть сделаны произвольные предположения. Несмотря на то, что они теоретически допустимы, вероятность их выполнения на практике очень низка. Использование этих предположений может привести к ложному предупреждению в качестве результата верификации. В данной статье мы делаем обзор на один из подходов, благодаря которому можно избавиться от такой проблемы, а также предлагаем формальное описание данного подхода в терминах формул путей, содержащих неинтерпретируемые функции, которые инструмент использует для моделирования памяти программы. Также мы приводим результаты сравнительного анализа эффективности предложенной реализации относительно существующей модели памяти.

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

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

Издание

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

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

DOI: 10.15514/ISPRAS-2017-29(4)-13

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