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 на трех спецификациях правил. Были выбраны следующие инструменты верификации:

• CPAchecker-RefSel – инструмент CPAchecker с конфигурацией на основе селективного уточнения — победитель в категории DeviceDriversLinux64.
• CPAchecker-LDV – CPAchecker в конфигурации LDV, которая используется по умолчанию в проекте LDV.
• BLAST – версии 2.7.3.

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

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

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