Институт системного программирования Роcсийской академии наук


Построение и использование 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.

В докладе будет изложена основная идея метода, рассказано об основных (наиболее простых) оптимизациях, использованных при его реализации, а также о более сложных оптимизациях, реализация которых планируется в будущем.

С презентацией доклада можно ознакомиться здесь.

Семинар группы

Технологии программирования

Перейти к списку семинаров ИСП РАН