@techreport{ball2000boolean,
author = {Ball, Thomas and Rajamani, Sriram},
title = {Boolean Programs: A Model and Process for Software Analysis},
institution = {Microsoft},
year = {2000},
month = {February},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/boolean-programs-a-model-and-process-for-software-analysis/},
number = {MSR-TR-2000-14},
}