Summary: BLAST (the Berkeley Lazy Abstraction Software verification Tool) is a verification system for checking safety properties of \(C\) programs using automatic property-driven construction and model checking of g of software abstractions. BLAST implements an abstract-model check-refine loop to check for reachability of a specified label in the program. The abstract model is built on the fly using predicate abstraction. This model is then checked for reachability. If there is no (abstract) path to the specified error label, BLAST reports that the system is safe and produces a succinct proof. Otherwise, it checks if the path is feasible using symbolic execution of the program. If the path is feasible, BLAST outputs the path as an error trace, otherwise, it uses the infeasibility of the path to refine the abstract model. BLAST short-circuits the loop from abstraction to verification to refinement, integrating the three steps tightly through “lazy abstraction”. This integration can offer significant advantages in performance by avoiding the repetition of work from one iteration of the loop to the next.
We now describe the algorithm in more detail. Internally, \(C\) programs are represented as control flow automata (CFA), which are control flow graphs with operators on edges. The lazy abstraction algorithm is composed of two phases. In the forward-search phase, we build a reachability tree, which represents a portion of the reachable, abstract state space of the program. Each node of the tree is labeled by a vertex of the CFA and a formula, called the reachable region, constructed as a boolean combination of a finite set of abstraction predicates. Initially the set of abstraction predicates is empty. The edges of the tree correspond to edges of the CFA and are labeled by basic program blocks or assume predicates. The reachable region of a node describes the reachable states of the program in terms of the abstraction predicates, assuming execution follows the sequence of instructions labeling the edges from the root of the tree to the node. If we find that an error node is reachable in the tree, then we go to the second phase, which checks if the error is real or results from our abstraction being too coarse (i.e., if we lost too much information by restricting ourselves to a particular set of abstraction predicates). In the latter case, we ask a theorem prover to suggest new abstraction predicates which rule out that particular spurious counterexample. The program is then refined locally by adding the new abstraction predicates only in the smallest subtree containing the spurious error; the search continues from the point that is refined, without touching the part of the reachability tree outside that subtree.
Thus the benefits are three-fold. First, we only abstract the reachable part of the state space, which is typically much smaller than the entire abstract state space. Second, we are able to have different precisions at different parts of the state space, which effectively means having to process fewer predicates at every point. Third, we avoid redoing the model checking over parts of the state space that we know are free of error from some coarser abstraction. Moreover, from the reachable set constructed by BLAST, invariants that are sufficient to prove the safety property can be mined, and a short, formal, easily checkable proof of correctness can be constructed. BLAST has successfully verified and found violations of safety properties of large device driver programs up to 60,000 lines of code. A beta version of BLAST has been released and is available from http://www.eecs.berkeley.edu/ tah/blast.
For the entire collection see [Zbl 1019.00013].