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

Одна из фундаментальных проблем в современных методах статической верификации программ состоит в точном учете семантики выражений с указателями. От точности анализа данных выражений зависит достоверность вердикта верификации. В данной работе описывается метод верификации с моделями памяти на основе неинтерпретируемых функций, который позволяет анализировать программы, содержащие выражения с указателями, в том числе указателями на структуры, массивы и выражения с адресной арифметикой. Ограничениями метода является конечность размера массивов и конечная глубина рекурсии для динамических структур данных. Предложенный метод был реализован в инструменте CPAchecker, основанном на подходе CEGAR с использованием булевой предикатной абстракции и интерполяции Крейга для получения новых предикатов при уточнении абстракции. Для решения задач проверки выполнимости формулы пути и интерполяции Крейга в CPAchecker используются интерполирующие решатели, поддерживающие бескванторные теории вещественной или целочисленной линейной арифметики и равенства с неинтерпретируемыми функциями. В разработанном подходе состояние памяти программы представляется в виде неинтерпретируемой функции, отображающей некоторые условные адреса переменных в памяти в их значения. При записи значения по какому-либо адресу происходит смена версии неинтерпретируемой функции, представляющей состояние памяти. Эксперименты проводились на наборах международных соревнований по верификации программ SV-COMP'2016, содержащих практически значимый набор из драйверов устройств ОС Linux. На этих наборах метод показывает приемлемые результаты по времени, сокращая при этом количество упущенных ошибок и ложных предупреждений. Среди возможных дальнейших направлений исследований отметим возможность более точного разбиения на регионы памяти, так что для этих регионов выделяются независимые неинтерпретируемые функции.