The BLAST tool implements a counterexample guided abstract model checking algorithm for model checking safety properties of C programs. A predicate abstraction of the C program is constructed on the fly along with the model checking, and the abstraction is refined locally using infeasible counterexample traces. The tool takes as input a C program and a safety monitor written in C syntax, and checks if the program satisfies the safety property specified by the monitor. If the property fails to hold, BLAST produces a counterexample trace in the source program witnessing the failure. If the property holds, the tool presents an easily checkable proof of correctness using program invariants found in the model checking. The process is automatic, in particular, no programmer annotations are required. We have used BLAST to model check safety properties of several Windows and Linux device drivers. We have found several bugs in the drivers, and provided short proofs for correct drivers.
We have extended the algorithm of BLAST in two directions: to check more expressive properties, and to work on concurrent programs. We have extended counterexample guided model checking to check controllability of linear time temporal logic properties. As a special case, this gives a counterexample guided model checking algorithm for linear time temporal logic verification (of which safety checking is a special case). We have also extended the implementation to check for race conditions in multi-threaded C programs using thread modular reasoning.