Counterexample-guided abstraction refinement for symbolic model checking

By Edmund M. Clarke, O. Grumberg, Somesh Jha, Yuan Lu, Helmut Veith. JACM, 2003

1,114 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Electrical and Electronic Engineering, Software

View Paper: https://www.semanticscholar.org/paper/d859b6698969b788bd25bc2abd96e6e57e341bea

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

1. Armando Solar-Lezama
2. Rastislav Bodík
3. Aaron R. Bradley
4. Hongseok Yang
5. Hakjoo Oh
6. A. Cimatti
7. Alberto Griggio
8. Andrea Micheli

In Electrical and Electronic Engineering

1. Aaron R. Bradley
2. Armando Solar-Lezama
3. Rastislav Bodík
4. Hongseok Yang
5. Hakjoo Oh
6. Shiva Prasad Kasiviswanathan
7. Alexey Ignatiev

In Software

1. Armando Solar-Lezama
2. Aaron R. Bradley
3. Hongseok Yang
4. Hakjoo Oh
5. A. Cimatti
6. Andrea Micheli
7. Marco Roveri
8. Alberto Griggio

Citations in the corpus

• An Abstraction-Refinement Approach to Verification of Artificial Neural Networks (2010, methodology): “While our approach is clearly inspired by counterexample guided abstraction-refinement (CEGAR) [7], in our case refinement is not guided by the counterexample, but just caused by it, so we speak of counterexample triggered abstraction-refinement (CETAR).”
• SAT-Based Model Checking without Unrolling (2011, methodology): “Our algorithm can be viewed from the perspective of predicate abstraction/refinement [17, 8]: the minor iterations generate new predicates (clauses) while the major iterations propagate them forward through the stepwise approximations (that is, add c ∈ F i to F i +1 if F i ∧ T ⇒ c ′ ).”
• Program synthesis by sketching (2008, background): “[18] to cope with the state explosion problem in model checking.”
• Model Checking and the State Explosion Problem (2011, methodology): “The counterexample-guided abstraction refinement (CEGAR) [10] technique uses counterexamples to refine an initial abstraction.”
• Verifying Properties of Binarized Deep Neural Networks (2017, methodology): “In particular, we use the idea of counterexample-guided search that is extensively used in formal verification (Clarke et al. 2003; McMillan 2005; 2003).”
• The nuXmv Symbolic Model Checker (2014, methodology): “All these techniques complement the “classical” counterexample guided (predicate) abstraction refinement (CEGAR) [22], also implemented in NUXMV.”
• Automatically generating features for learning program analysis heuristics for C-like languages (2017, methodology): “Addressing these concerns with manually-designed heuristics has been the goal of a large body of research in the program-analysis community [Ball and Rajamani 2002; Clarke et al. 2003; Grebenshchikov et al. 2012; Gulavani et al. 2008; Gupta et al. 2013; Henzinger et al. 2004; Kastrinis and Smaragdak”