LDV Validator¶

LDV Validator is a tool for validating LDV Tools verification system, in particular its back ends, i.e. verifiers like BLAST or CPAchecker. An approach, implemented in LDV Validator, is that LDV Tools are tried to find some known bugs in programs. If known bugs can be found using appropriate specifications, then we prove that LDV Tools and corresponding verifiers work good. Otherwise we have reasons to revise LDV Tools or/and verifiers (sometimes we can have bugs in specifications as well), since this means that we can miss bugs during verification in production.

Sources of programs with known bugs¶

One of the most simplest approach to get programs with bugs is to introduce these bugs by ourselves. We used this approach very widely in preparing test cases for LDV tools specifications. It is obviously, that we can''t cover all possible situations with these test cases. Thus we need other sources of programs with known bugs for validating LDV Tools.

We found out that programs with known nonartificial bugs can be efficiently obtained on the basis of the Linux kernel repositories. We have analyzed about 3 thousands of commits made to stable branches of the Linux kernel. This allowed us to find about 400 of nonfunctional bugs. And about 50% of these bugs were related with Linux kernel API misuse - exactly those bugs which can be found with help of LDV Tools. Information on those bugs (commit hashes, module names, specification identifiers, etc.) was put to a configuration file. LDV Validator gets that file as input and automatically launches LDV Tools with specified verifier, obtains verification results and generates a report where you can find summary information on all known bugs as well as details on whether a particular bug was detected or not. Besides LDV Validator automatically checks Linux kernel modules after fixing bugs. This aids to understand whether LDV Tools or/and a verifier did find a bug fixed in corresponding commit.