Lazy Abstraction* Thomas A. Henzinger Ranjit dhala Rupak Majumdar EECS Department, University of California Berkeley, CA 94720-1770, U.S.A. {tab_, j hala, rupak}@eecs, berkeley, edu Gregoire Sutre LaBRI, Universit6 de Bordeaux 1 33405 Talenee Codex, France sutre@labri, u-bordeaux, fr ABSTRACT One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, re- fine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-cheek-refine loop. Lazy abstraction continu- ously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algo- rithm for model checking safety properties using lazy ab- straction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method. 1. INTRODUCTION While model checking [11] has made significant inroads in hardware verification, a renewed focus on model checking for software has emerged only in the past couple of years. We believe that this renewed attention has been helped signifi- cantly by two related trends: first, modern model checking is increasingly viewed more broadly than state enumeration or BDD crunching, namely, as computation with predicates that represent state sets (keywords "predicate abstraction" [20], "symbolic transition systems" [22], "constraint-based model checking" [14]); second, the performance of decision procedures and theorem provers for relevant predicate theo- ries (e.g., booleans, Presburger, arrays) and their combina- tions has been steadily improving [15, 25, 27]. *This work was supported in part by the NSF ITR grant CCR-0085949, the NSF Theory grant CCR-9988172, the DARPA PCES grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660, and the SRC contract 99-TJ- 683.003. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. POPL 7)2, January 16-18, 2002, Portland, Oregon, USA. Copyright 2002 ACM 1-58113-450-9/02/01 ..$5.00 One traditional flow for model checking a piece of code proceeds through the following loop [5, 10, 28]: Step i ("abstraction") A finite set of predicates is chosen, and an abstract model of the given program is built au- tomatically as a finite or push-down automaton whose states represent truth assignments for the chosen pred- icates. Step 2 ("verification") The abstract model is checked au- tomatically for the desired property. If the abstract model is error-free, then so is the original program (re- turn "program correct"); otherwise, an abstract eoun- terexample is produced automatically which demon- strates how the model violates the property. Step 3 ("counterexample-driven refinement") It is checked automatically if the abstract eounterexample corre- sponds to a concrete eounterexample in the original program. If so, then a program error has been found (return "program incorrect"); otherwise, the chosen set of predicates does not contain enough information for proving program correctness and new predicates must be added. The selection of such predicates is au- tomated, or at least guided, by the failure to concretize the abstract counterexample [i0]. Goto Step i. The problem with this approach is of course that both Step 1 and Step 2 are eomputationally hard problems, and with- out additional optimizations, the method does not scale to large systems. We believe that in order to evaluate the full promise of this approach, the loop from abstraction to ver- ification to refinement should be short-circuited. We show that all three steps can be integrated tightly through a con- cept we call "lazy abstraction," and that this integration can offer significant advantages in performance, by avoiding the repetition of work from one iteration of the loop to the next. Intuitively, lazy abstraction proceeds as follows. In Step 3, call the abstract state in which the abstract eounterexam- ple fails to have a concrete counterpart, the pivot state. The pivot state suggests which predicates should be used to refine the abstract model. However, instead of building an entire new abstract model, we refine the current abstract model "from the pivot state on." Since the abstract model may 58contain loops, such refinement on demand may, of course, refine parts of the abstract model that have already been constructed, but it will do so only if necessary; that is, if the desired property can be verified without revisiting some parts of the abstract model, then our algorithm succeeds in doing so. The algorithm integrates all three steps by con- strueting and verifying and refining on-the-fly an abstract model of the program, until either the desired property is established or a concrete eounterexample is found. Upon termination with the outcome "program correct," the proof is not an abstract model on a global set of predicates, but an abstract model whose predicates change from state to state. Thus, lazy abstraction combats the computational diffi- eulties of Steps i and 2 in the following way. Abstraction is done on-the-fly, and only up to the precision necessary to rule out spurious eounterexamples. On-the-fly construction of an abstract transition system eliminates an often waste- ful and expensive model-construction phase; model checking only the "current" portion of the abstract transition system saves the cost of unnecessary exploration in parts of the state space that are already known to be free of errors. It is easy to envision extreme eases in which our algorithm achieves large savings. Suppose, for example, that the