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

user warning: Got error 28 from storage engine query: SELECT t.*,v.weight AS v_weight_unused FROM term_node r INNER JOIN term_data t ON r.tid = t.tid INNER JOIN vocabulary v ON t.vid = v.vid WHERE r.vid = 264 ORDER BY v.weight, t.weight, t.name in /opt/drupal-6.33/modules/taxonomy/taxonomy.module on line 640.

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:

Results of running tools on the drivers from the Linux kernel 4.4-rc1

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 verdicts 872 402
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.

Predicate Analysis with BLAST 2.7.3