Моделирование памяти при верификации программ методом CEGAR

Михаил Мандрыкин. Начало семинара - 29 января 2013 г.

Об инструментировании и генерировании окружения для драйверов, верифицируемых в системе Linux Driver Verification (LDV) было рассказано на предыдущих семинарах. Проверка же подготовленного кода драйвера, вместе со сгенерированным окруженем, в среде LDV в настоящее время осуществляется инструментами статического анализа кода, такими как CPAchecker и BLAST. В основе работы этих инструментов лежит подход CEGAR -- уточнение абстракции по контрпримерам. В докладе будет рассмотрена общая идея работы этого подхода, выделены его основные преимущества и недостатки по сравнению с другими широко используемыми методами статической верификации (BMC, shape-analysis), а затем рассказано об одном из направлений улучшения точности верификации -- моделировании указателей с помощью функций или массивов. Также в докладе будет рассказано о результатах применения инструментов CPAchecker и BLAST в проекте LDV и результатах соревноваий среди статических верификаторов (SV-COMP) в 2012-2013 гг.

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

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

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

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