Counterexample-Guided Abstraction Refinement
Lecture notes in computer sciencePublished 1 January 2000Open access
Edmund M. Clarke, Orna Grümberg, Somesh Jha, Yuan Lu, Helmut Veith
Citations1,649
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
Abstract
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.
Keywords
Computer Science
Abstract interpretation
6,131 Citations1977Patrick Cousot, Radhia Cousot
Lecture notes in computer scienceCounterexample-Guided Abstraction Refinement
1,649 Citations2000Edmund M. Clarke, Orna Grümberg +3 more
Lecture notes in computer scienceConstruction of abstract state graphs with PVS
1,471 Citations1997Susanne Graf, Hassen Saı̈di
This paper proposes a method for the automatic construction of an abstract state graph of an arbitrary system using the Pvs theorem prover.
ACM Transactions on Programming Languages and SystemsModel checking and abstraction
1,217 Citations1994Edmund M. Clarke, Orna Grümberg +1 more
Using techniques similar to those involved in abstract interpretation, an abstract model of a program is constructed without ever examining the corresponding unabstracted model, and it is shown how this abstract model can be used to verify properties of the original program.
Computers & Mathematics with ApplicationsComputer-aided verification of coordinating processes: The automata-theoretic approach
793 Citations1995
International Journal on Software Tools for Technology TransferNUSMV: a new symbolic model checker
716 Citations2000Alessandro Cimatti, Edmund M. Clarke +2 more
A new symbolic model checker, called NuSMV, developed as part of a joint project between CMU and IRST, and a detailed description of its functionalities, architecture, and implementation is described.
Symbolic model checking using SAT procedures instead of BDDs
688 Citations1999Armin Biere, Alessandro Cimatti +3 more
This paper applies bounded model checking to equivalence and invariant checking and presents several optimizations that reduce the size of generated propositional formulas in hardware verification.
Lecture notes in computer scienceNuSMV: A New Symbolic Model Verifier
605 Citations1999Alessandro Cimatti, Emma L. Clarke +2 more
NUSMV, a new symbolic model checker developed as a joint project between Carnegie Mellon University and Istituto per la Ricerca Scientifica e Tecnolgica (IRST), is described, a well structured, open, flexible and documented platform for model checking.
Symbolic Model Checking without BDDs
532 Citations1999Armin Biere, Alessandro Cimatti +2 more
Princeton University Press eBooksComputer-Aided Verification of Coordinating Processes
441 Citations1995Robert P. Kurshan
Theories of L-automaton/L-process, L-matrix, and String Acceptors are compared to Boolean Algebra, which describes the construction of language-based Algebra.
Lecture notes in computer scienceCorrect Hardware Design and Verification Methods
377 Citations1999Marius Bozga, Oded Maler
Lecture notes in computer scienceExperience with Predicate Abstraction
235 Citations1999Satyaki Das, David L. Dill +1 more
This reports some experiences with a recently-implemented prototype system for verification using predicate abstraction, based on the method of Graf and Saidi, applied successfully to two nontrivial examples: the Flash multiprocessor cache coherence protocol, and a concurrent garbage collection algorithm.
Lecture notes in computer scienceProgress on the State Explosion Problem in Model Checking
195 Citations2001Edmund M. Clarke, Orna Grümberg +3 more
This aim of this paper is to give a succinct survey of symbolic model checking and to introduce the reader to recent advances in abstraction.
Lecture notes in computer scienceAbstract and Model Check while You Prove
167 Citations1999Hassen Saı̈di, Natarajan Shankar
This work shows how boolean abstractions can be constructed simply, efficiently, and precisely for infinite state systems while preserving properties in the full µ-calculus, and proposes an automatic refinement algorithm which refines the abstraction until the property is verified or a counterexample is found.
Lecture notes in computer scienceSAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques
144 Citations2002Edmund M. Clarke, Anubhav Gupta +2 more
New techniques for model checking in the counterexample guided abstraction/refinement framework are described, which use a combination of Integer Linear Programming (ILP) and machine learning techniques for refining the abstraction based on the counteretxample.
Tree-like counterexamples in model checking
140 Citations2003E. M. Clarke, Somesh Jha
A new general framework for counterexamples is introduced and it is shown that a large class of temporal logics beyond ACTL admits countereXamples with a simple tree-like transition relation, related to a universal fragment of extended branching time logic based on w-regular temporal operators.
Lecture notes in computer scienceIncompleteness, Counterexamples, and Refinements in Abstract Model-Checking
119 Citations2001Roberto Giacobazzi, Elisa Quintarelli
This paper gives a constructive characterization of Clarke et al.'s spurious counterexamples in terms of both forward and backward completeness of the underlying abstract interpretation, and applies this result to improve static program analysis by refining the model-checking of an abstract interpretation.
Successive approximation of abstract transition relations
112 Citations2002Satyaki Das, David L. Dill
Recently, the efficiency of the predicate abstraction scheme presented by Das, Dill and Park (1999) has been improved, and the number of validity checks needed to prove the necessary verification condition has been reduced.
Lecture notes in computer scienceVerification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement
103 Citations2003Edmund M. Clarke, Ansgar Fehnker +4 more
This paper presents a new procedure to perform this refinement operation for abstractions of infinite-state systems, in particular of hybrid systems, and shows reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently.
Lecture notes in computer scienceCounter-Example Based Predicate Discovery in Predicate Abstraction
85 Citations2002Satyaki Das, David L. Dill
A method of discovering most of these predicates automatically by analyzing spurious abstract counter-example traces is demonstrated and has been applied to a simplified version of the Ad hoc On-Demand Distance Vector Routing protocol where it successfully discovers all required predicates.
Lecture notes in computer scienceA Performance Study of BDD-Based Model Checking
85 Citations1998Bwolen Yang, Randal E. Bryant +6 more
One of the main conclusions of this work is that the BDD computations in model checking and in building BDDs for the outputs of combinational circuits have fundamentally different performance characteristics.
Lecture notes in computer scienceCounterexample-Guided Control
78 Citations2003Thomas A. Henzinger, Ranjit Jhala +1 more
This work presents a counterexample-guided refinement algorithm for solving ω-regular control objectives, which is fully symbolic, and therefore applicable also to infinite-state systems.
Lecture notes in computer scienceIncremental Verification by Abstraction
77 Citations2001Yassine Lakhnech, Saddek Bensalem +2 more
A uniform verification method that combines abstraction, model-checking and deductive verification in a novel way is presented that allows and shows how to use the set of reachable states of the abstract system in a deductive proof even when the abstract model does not satisfy the specification.
Lecture notes in computer scienceAn iterative approach to language containment
76 Citations1993Felice Balarin, Alberto Sangiovanni‐Vincentelli
An iterative approach to formal verification by language containment is proposed, which starts with some initial abstraction and then iteratively refine it, guided by the failure report from the verification tool.
Lecture notes in computer scienceMultiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation
56 Citations2003Marcelo Glusman, Gila Kamhi +3 more
A completely automated framework for iterative abstraction refinement that is fully integrated into a formal-verification environment and demonstrates the effectiveness of the framework on challenging Intel designs that were not amenable to BDD-based model-checking approaches.
Verifying IP-core based system-on-chip designs
53 Citations2003Pankaj Chauhan, E. M. Clarke +2 more
In this work, the problem of verifying system-on-chip designs is decomposed into three tasks, and the standard bus interconnecting IP cores in the system are verified once and for all.
Tearing based automatic abstraction for CTL model checking
53 Citations1996Woohyuk Lee, Abelardo Pardo +3 more
Electronic Notes in Theoretical Computer ScienceAutomated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach
45 Citations2003Sagar Chaki, Joël Ouaknine +2 more
A fully automated compositional framework which combines two orthogonal abstraction techniques within a counterexample-guided abstraction refinement (CEGAR) scheme which incrementally increases the granularity of the abstractions until the specification is either established or refuted.
Lecture notes in computer scienceStepwise CTL Model Checking of State/Event Systems
39 Citations1999Jørn Lind-Nielsen, Henrik Reif Andersen
An efficient technique for symbolic model checking of any CTL formula with respect to a state/event system is presented, which is a concurrent version of a Mealy machine and is used to describe embedded reactive systems.
Incremental CTL model checking using BDD subsetting
37 Citations1998Abelardo Pardo, Gary D. Hachtel
An automatic abstraction/refinement algorithm for symbolic CTL model checking is presented and is done for the full CTL language-no restriction is made to the universal or existential fragments.
Verification by approximate forward and backward reachability
32 Citations1998S. Govindaraju, David L. Dill
The idea of approximations using overlapping projections to symbolic backward reachability is extended and a simple heuristic is given, which seems to work well in practice, for generating a counter-example path from this approximation.
Lecture notes in computer scienceSymbolic Localization Reduction with Reconstruction Layering and Backtracking
23 Citations2002Sharon Barner, Daniel Geist +1 more
Using algorithmic improvements to localization reduction, a new symbolic algorithm for path reconstruction including incremental refinement and backtracking is presented that was able to verify circuits that were not previously able to address.
Lecture notes in computer scienceAbstract BDDs: A Technique for Using Abstraction in Model Checking
16 Citations1999Edmund M. Clarke, Somesh Jha +2 more
This work proposes a new methodology for exploiting abstraction in the context of model-checking that uses abstract BDDs as its underlying data structure and shows that this technique builds a more refined model than traditional compiler-based methods proposed by Clarke, Grumberg and Long.
An approach to verify a large scale system-on-a-chip using symbolic model checking
13 Citations2002K. Takayama, Toyomi Satoh +2 more
A new verification methodology based on a "navigated" model checking that can verify designs without ad-hoc simplification and also can check various possible paths relating the error, instead of concentrating on a particular path of the trace.
Automatic abstraction techniques for formal verification of digital systems
8 Citations1998Abelardo Pardo-Sanchez
This dissertation proposes an automatic abstraction paradigm to verify generic digital systems and presents an abstraction theory in the context of model checking of the $\mu$-calculus logic, which provides a conservative answer to the verification problem.