Predicate abstraction refinement in thread-modular analysis

Комбинация анализа с раздельным рассмотрением потоков (Thread-Modular analysis) и предикатной абстракции является эффективной техникой верификации реального программного обеспечения. Одним из недостатков этой техники является уточнение предикатной абстракции при анализе многопоточных программ. В классической процедуре уточнения абстракции рассматривается только путь в одном потоке, и окружение Thread-Modular анализа не уточняется. Например, при применении эффекта из второго потока к первому путь к эффекту во втором потоке не уточняется. Целью нашей работы была разработка более точной процедуры уточнения абстракции, которая бы переиспользовала имеющуюся процедуру уточнения абстракции и позволяла бы уточнять и путь в анализируемом потоке, и путь в окружении. Основная идея заключается в построении совместной логической формулы для двух путей. Так как имена переменных разных потоков могут совпасть, необходимо корректно переименовать и приравнять некоторые переменные для того, чтобы формула правильно отражала связи между потоками. Это позволяет получить предикаты, необходимые для доказательства недостижимости пути. Предложенный подход был реализован на базе инструмента статической верификации CPAchecker. Подход был оценен на стандартном наборе задач SV-COMP и показал небольшое улучшение. Для больших программ улучшений в результатах не наблюдалась, так как описанный недостаток анализа не является единственной причиной ложноположительных результатов. Предложенный подход может успешно доказать недостижимость некоторых путей, то этого может быть недостаточно для доказательства корректности программы. Однако подход обладает дальнейшим потенциалом для совершенствования.