Abstraction is fundamental in combating the state explosion problem in model checking. Automatic techniques have been developed that eliminate presumed irrelevant detail from a model and then refine the abstraction until it is accurate enough to prove the given property. This abstraction refinement approach, initially proposed by Kurshan, has received great impulse from the use of efficient satisfiability solvers in the check for the existence of error traces in the concrete model. Today it is widely applied to the verification of both hardware and software. For complex proofs, the challenge is to keep the abstract model small while carrying out most of the work on it. We review and contrast several refinement techniques that have been developed with this objective. These techniques differ in aspects that range from the choice of decision procedures for the various tasks, to the recourse to syntactic or semantic approaches (e.g., “moving fence” vs. predicate abstraction), and to the analysis of bundles of error traces rather than individual ones.


Mathematical Logic Model Check Software Engineer Decision Procedure Formal Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Fabio Somenzi
    • 1
  1. 1.University of Colorado at Boulder 

Personalised recommendations