Computer Science Department
School of Computer Science, Carnegie Mellon University
Counterexample-guided Abstraction Refinement
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
Keywords: Abstraction, model checking, counterexample
We present an automatic iterative abstraction-refinement methodology in which
the initial abstract model is generated by an automatic analysis of the
control structures in the program to be verified. Abstract models may
admit erroneous (or "spurious") counterexamples. We devise new symbolic
techniques which analyze such counterexamples and refine the abstract
model correspondingly. The refinement algorithm keeps the size of the
abstract state space small due to the use of abstraction functions
which distinguish many degrees of abstraction for each program variable.
We describe an implementation of our methodology in NuSMV.
Practical experiments including a large Fujitsu IP core design with about
500 latches and 10000 lines of SMV code confirm the
effectiveness of our approach.