Counterexample-Guided Abstraction Refinement

By Edmund M. Clarke, O. Grumberg, Somesh Jha, Yuan Lu, Helmut Veith. International Conference on Computer Aided Verification, 2000

1,787 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/1d8e5b1674f94dceea8af0b4a641d2f269956c48

How researchers see this paper

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

Citations in the corpus

Abstract Regular Model Checking (2004, background): “Indeed, this is the way large (or infinite) state spaces are being successfully handled outside the domain of regular model checking using the so-called abstract-check-refine paradigm [20, 26, 14, 16] implemented, e.”
Modular verification of software components in C (2003, methodology): “The MAGIC tool follows the well-known abstract - verify - refine paradigm [13, 16, 21, 27]:”
Liquid types (2008, background): “, there is an error) or if not, to lazily extract new qualifiers from the counterexample [6, 3, 16].”
Boolean and Cartesian abstraction for model checking C programs (2001, background): “In principle, Phases (2) and (3) will follow the lines of other work on interprocedural program analysis [19, 23], and abstraction refinement [4, 15]).”
Tools and Algorithms for the Construction and Analysis of Systems (2003, unknown): “An high-level view of the Bounded Model Checker module in NuSMV For example, in the case of the formula F(x = 2 ∧O(x = 3 ∧O(x = 4 ∧O(x = 5)))) presented in Section 5.1, the encoding is able to perform a “virtual” unrolling of the (6,2)-path up to time 14 with no necessity of introducing more than 7 ”
WYSINWYX: What you see is not what you eXecute (2010, methodology): “In source-code analysis, abstraction re.nement [Kurshan 1994; Clarke et al. 2000] is a well-known technique for enhancing precision.”
The software model checker Blast (2007, methodology): “A key paradigm behind some of the new software verification tools is the principle of counterexample-guided abstraction refinement (CEGAR) [1,3,4, 21 ,49,61,78].”
SATABS: SAT-Based Predicate Abstraction for ANSI-C (2005, methodology): “This is automated by Counterexample Guided Abstraction Refinement [5, 6, 7].”
Abstractions from proofs (2004, background): “These start with some coarse abstract domain and successively refine the domain by adding facts that make the abstraction sufficiently precise to refute spurious counterexamples [4, 5, 8, 12, 19].”
A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “In counterexample-guided abstraction refinement [87], [ 37 ], [7] (CEGAR), if model checking the abstraction yields a counterexample that does not exist in the concrete program, the abstract counterexample is”
Secure two-party computations in ANSI C (2012, background): “As explained above, CBMC reads a C program f containing assertions along with a bound k, and generates a Boolean constraint Bf in CNF such that the satisfying assignments of Cf encode program traces of size at most k that violate the assertions.”
Verifying Properties of Binarized Deep Neural Networks (2017, methodology): “While these encodings could be directly handled by modern SAT solvers, we show that one can exploit the structure of these encodings to solve the resulting SAT formulas more efﬁciently based on the idea of counterexample-guided search (Clarke et al. 2000).”
Introduction to Embedded Systems - A Cyber-Physical Systems Approach (2013, methodology): “An effective and widely-used technique is counterexample-guided abstraction refinement (CEGAR), first introduced by Clarke et al. (2000). The basic idea (when using localization reduction) is to start by hiding almost all state variables except those referenced by the temporal logic property.”
Thorough static analysis of device drivers (2006, background): “This harness leads to fewer false errors being reported but results in increased analysis times.”