11.04.2016: BLAST 2.7.3 на SV-COMP'2016

BLAST 2.7.3 был представлен на пятых международных соревнованиях по верификации программ, которые прошли в рамках конференции TACAS 2016 в Эйндховене, Нидерланды. В этом году BLAST выиграл бронзу в категории DeviceDriversLinux64.

BLAST – это классический инструмент статической верификации программ, основанный на предикатных абстракциях и методе CEGAR. Он поддерживается ИСП РАН и активно используется в проекте Linux Driver Verification (LDV).

В рамках проекта LDV мы провели эксперименты на драйверах ядра ОС Linux 4.4-rc1 на трех спецификациях правил. Были выбраны следующие инструменты верификации:

Результаты запуска инструментов верификации на драйверах ядра ОС Linux 4.4-rc1

По результатам, представленным в таблице, мы видим, что BLAST требует меньше времени чем CPAchecker и находит больше вердиктов unsafe, но находит меньше вердиктов safe. Инструмент CPAchecker в конфигурации LDV на драйверах показал результаты лучше чем CPAchecker-RefSel, поэтому мы выберем его для детального сравнения с BLAST.

В таблице ниже показано количество корректных вердиктов, найденных только с помощью CPAchecher-LDV или только с помощью BLAST. Таким образом, для инструмента CPAchecker включаются все переходы из вердиктов unknown, некорректных safe и unsafe, найденных BLAST, в корректные вердикты safe и unsafe, найденные CPAchecker-LDV. Строка корректные вердикты unsafe включает только переходы в корректные вердикты unsafe.

Только с помощью CPAchecker‑LDV Только с помощью BLAST 2.7.3
Корректные вердикты 872 402
Корректные вердикты unsafe (ошибки) 57 80

Из таблицы можно видеть, что CPAchecker находит больше корректных вердиктов, а также новые ошибки, количество которых меньше чем для инструмента BLAST. На данный момент CPAchecker является нашим основным инструментом верификации, но BLAST все еще полезен для обнаружения ошибок.

Predicate Analysis with BLAST 2.7.3