The Holy Grail of Computer Science: Automatic Program Verification

Thomas Henzinger
University of California, Berkeley, Ecole Polytechnique Fédérale de Lausanne
Friday, 28 May, 2004 (All day)

While model checking has entered industrial practice in hardware verification for some time now, the original goal of model checking ---namely, software verification--- has proved elusive until recently. One of the main reasons is that boolean finite-state abstractions are readily available for circuits, but not for programs. A central problem in software verification is to find an abstraction of the input program which is sufficiently fine to prove or disprove the desired property, and yet sufficiently coarse not to overwhelm the exhaustive exploration of the state space performed by a model checker. It is often useful to abstract the values of program variables by recording, instead, at each program location the truth of critical predicates. The critical predicates can be found automatically using counterexample-guided abstraction refinement, which starts with a coarse abstraction of the program and iteratively refines the abstraction until either an error trace is found or the property is proved.

The BLAST project has improved this approach in three significant ways. First, the program abstraction is constructed lazily, which means that a critical predicate is evaluated only at those program locations where its value is relevant. While for a large piece of software, hundreds of predicates may be critical, at any given location typically less than 10 of these predicates are relevant. Second, BLAST finds critical predicates by Craig interpolation, which means that each predicate is an assertion about the current values of program variables at a location. Computed in this way, predicates do not encode the history of a program trace but rather capture exactly the relevant current state information at each program location. Third, in order to handle multi-threaded programs, BLAST deals with one thread at a time and automatically infers a context assumption for each thread, which summarizes the interference caused by the other threads. The context assumptions, in turn, are automatically discharged by assume-guarantee reasoning.

Given a C program and a temporal safety property, BLAST provides either a test vector that exhibits a violation of the property, or a succinct proof certificate in the form of an abstract reachability tree, which can be reused incrementally for checking updated versions of the program. The tool has been applied successfully to Linux and Windows device drivers and NesC protocols with tens of thousands of lines of C code.

The BLAST project is the work of Ranjit Jhala, Rupak Majumdar, Dirk Beyer, Shaz Qadeer, Marco Sanvido, and Gregoire Sutre.