Predicate abstractions memory modeling method with separation into disjoint regions

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