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.
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.
|Only by CPAchecker‑LDV||Only by BLAST 2.7.3|
|Correct unsafe verdicts (bugs)||57||80|
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.