We describe abstraction based model checking techniques that compute under approximations of the feasible behaviors of the system under analysis. The techniques preserve errors to safety properties, since all analyzed behaviors are feasible by definition. The techniques perform model checking with explicit, or symbolic, execution and abstract state matching. They do not require an abstract transition relation to be generated, but instead execute the concrete transitions while storing abstract versions of the explored states, as specified by an abstraction mapping. State matching determines whether an abstract state is being revisited, in which case the model checker backtracks. Applications include program error detection and test input generation.

We first present an abstraction refinement method which performs explicit execution with abstract state matching, as specified by a set of abstraction predicates. We then discuss abstract state matching for model checking with symbolic, rather than explicit, execution. We evaluate the techniques in the context of test input generation for Java containers.

This is joint work with Saswat Anand (Georgia Institute of Technology), Radek Pelanek (Masaryk University) and Willem Visser (RIACS/NASA Ames).

Corina Pasareanu is a research scientist at NASA Ames Research Center, in the Robust Software Engineering group. She is employed by QSS. Her research interests are in software verification. She is currently investigating the use of abstraction and symbolic execution in the context of the Java PathFinder model checker, with applications in test input generation and error detection. She is also working on automating assume guarantee style reasoning for compositional verification. She received her PhD degree from Kansas State University. More information can be found at http://ic.arc.nasa.gov/people/pcorina/, and she can be contacted on pcorina@email.arc.nasa.gov.