27-Aug-2014: Version 0.6 of LDV Tools released

LDV Tools 0.6 includes the following most important changes:

Results of validation of LDV Tools 0.6 and LDV Tools 0.5 with different verification tools on 41 known bugs in the Linux kernel* are presented in the table below.

LDV Tools 0.6 LDV Tools 0.5
BLAST CPAchecker BLAST CPAchecker
Found bugs 17 13 15 14
Missed bugs Bugs in verification tools 3 2 3 3
Out of memory (63 gigabytes) 1 2 1 0
Timeouts (50 minutes) 0 6 0 4
Unsupported rule specifications 0 0 7 7
Others 20 18 15 13

Both BLAST and CPAchecker were able to find one more bug thanks to improvements in rule specification SKB allocation in pm_runtime context. Additionally BLAST has found a new bug with one of the new rule specifications. CPAchecker has lost ability to detect 3 bugs due to degradation in analysis time, while it has found a bug that led to an exception before.

The source code repository can be browsed by v0.6 tag. To get and to install LDV Tools see instructions.

* This validation benchmark has many differences from the one used earlier for validating LDV Tools 0.5.