Counter-Example Guided Abstraction Refinement is a method of constructing an abstraction of a system such as a program by constructing a series of increasingly precise abstractions, attempting to verify the system using those abstractions and, if an attempt fails, using a counter-example from the failed attempt to construct a more precise abstraction.
I think the original paper was clarke:cav:2000.
Notes related to CEGAR (Counter-Example Guided Abstraction Refinement)
Papers related to CEGAR (Counter-Example Guided Abstraction Refinement)
- Automatic predicate abstraction of C programs [ball:pldi:2001]
- Model checking: Algorithmic verification and debugging [clarke:cacm:2009]
- Counterexample-guided abstraction refinement [clarke:cav:2000]
- Software verification with BLAST [henzinger:spin:2003]
- Software model checking [jhala:compsurv:2009]