Сборники трудов ИСП РАН


Введение в метод CEGAR — уточнение абстракции по контрпримерам.

М.У. Мандрыкин, В.С. Мутилин, А.В. Хорошилов.

Аннотация

Точность, полнота и масштабируемость применяемых на практике инструментов статической верификации значительно возросла за последнее десятилетие. В частности, успешный автоматизированный анализ программных систем среднего размера с использованием проверки моделей, получаемых при помощи предикатной абстракции, стал возможен благодаря развитию метода уточнения абстракции по контрпримерам — CEGAR (Counter Example Guided Abstraction Refinement). Этот метод так или иначе используется в таких инструментах, как SLAM, BLAST, SATABS и CPAchecker. В рамках данной статьи мы рассмотрим метод CEGAR в том виде, как он реализован в инструментах статической верификации BLAST и CPAchecker.

Ключевые слова

статическая верификация, предикатная абстракция, проверка моделей, уточнение абстракции по контрпримерам, интерполяция Крейга, крупноблочное кодирование

Издание

Труды Института системного программирования РАН, том 24, 2013, стр. 219-292.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2013-24-12

Полный текст статьи в формате pdf Вернуться к содержанию тома