Lazy Abstraction

One approach to model checking software is based on the abstract-check-re ne paradigm: build an abstract model, then check the desired property, and if the check fails, re- ne the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-re ne loop. Lazy abstraction continuously builds and re nes a single abstract model on demand, driven by the model checker, so that dierent parts of the model may exhibit dierent degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sucient conditions for the termination of the method