11-Apr-2016: BLAST 2.7.3 at SV-COMP'2016

BLAST 2.7.3 was presented at the 5th International Competition on Software Verification (SV-COMP) held at TACAS 2016 in Eindhoven, Netherlands. This year BLAST has won the bronze medal in the DeviceDriversLinux64 category.

BLAST is a classic software model checking tool based on predicate abstractions and CEGAR. It is maintained by ISPRAS as long as it is actively used within Linux Driver Verification (LDV) project.

As a part of LDV we conducted experiments on the drivers from the Linux kernel 4.4-rc1 on three rule specifications. We have chosen the following tools:

• CPAchecker-RefSel – CPAchecker based on refinement selection configuration. The winner in DeviceDriversLinux64 category.
• CPAchecker-LDV – CPAchecker in LDV configuration which is used by default in LDV project.
• BLAST – version 2.7.3.

From the total results table we can see that the BLAST requires less time than CPAchecker and finds more unsafe verdicts, but finds less safe verdicts. CPAchecker in LDV configuration has shown better results on drivers than CPAchecker-RefSel, so we consider this configuration in detail for comparison with BLAST.

In the table below we show the number of correct verdicts found only by CPAchecher-LDV or by BLAST. Thus, for CPAchecker it includes all trasitions from unknowns, incorrect safes and unsafes found by BLAST to correct safes and unsafes found by CPAchecker-LDV. The row correct unsafe verdicts includes only transitions to correct unsafes.

From the table we can see that CPAchecker has more correct results and finds new correct bugs, but less than BLAST. Now CPAchecker is our main verification tool, but BLAST still fits as a fiddle.