A fundamental issue in model checking of software is the choice of a model for software. We present a model called boolean programs that is expressive enough to represent features in common programming languages and is amenable to model checking. We present a model checking algorithm for boolean programs using context-free-language reachability. The model checking algorithm allows procedure calls with unbounded recursion, exploits locality of variable scopes, and gives short error traces. Furthermore, we give a process for incrementally refining an initial skeletal boolean program B (representing a source program P ) with respect to a particular reachability query in P . The presence of infeasible paths in P may lead to the model checker reporting false positive errors in B . We show how to refine B by introducing boolean variables to rule out the infeasible paths. The process uses ideas from model checking, symbolic execution, and program slicing.

PostScript file

PDF file

Details