Построение и использование SMT-формул с неинтерпретируемыми функциями для уточнения предикатной абстракции в инструменте CPAchecker
Построение и использование SMT-формул с неинтерпретируемыми функциями для уточнения предикатной абстракции в инструменте CPAchecker
Мандрыкин Михаил. Начало семинара - 19 февраля 2014 г.Работа с указателями и динамической памятью до сих пор остается одной из плохо поддерживаемых возможностей во многих инструментах автоматической статической верификации, реализующих метод CEGAR с предикатной абстракцией. В соревнованиях автоматических статических верификаторов SV-COMP'14 из 5 участников, использующих CEGAR с предикатной абстракцией, только 2 участвовало в категории HeapManipulation, состоящей из заданий, проверяющих поддержку динамической памяти. При этом один из этих инструментов занял в данной категории последнее место. В то же время инструменты, основанные на CEGAR с предикатной абстракцией, используются для верификации драйверов операционных систем (например, драйверов Linux в проекте LDV), в которых указатели, в том числе на динамическую память, используются очень активно.
В рамках проекта LDV в инструменте CPAchecker была реализована поддержка работы с указателями и динамической памятью в рамках метода CEGAR с предикатной абстракцией. Реализованный метод основывается на оптимизированном кодировании предполагаемых ошибочных путей, используемых для итеративного построения предикатной абстракции, в логические SMT-формулы, значительно использующие теорию неинтерпретируемых функций. Использование такого метода, в частности, позволило инструменту CPAchecker показать в категории HeapManipulation результаты, близкие к результатам инструментов, использующим более "тяжеловесные" (то есть ресурсоемкие), чем CEGAR подходы -- Bounded Model Checking и Shape Analysis. В рамках проекта LDV идет работа по применению модифицированного инструмента CPAchecker для более точной верификации драйверов ОС Linux.
В докладе будет изложена основная идея метода, рассказано об основных (наиболее простых) оптимизациях, использованных при его реализации, а также о более сложных оптимизациях, реализация которых планируется в будущем.
С презентацией доклада можно ознакомиться здесь.