Counterexample-Guided Abstraction Refinement
Counterexample-Guided Abstraction Refinement is a scholarly work by Edmund M. Clarke, published in 2000 in ''Lecture Notes in Computer Science''. The main subjects of the publication include abstraction, formal methods, Abstraction model checking, test automation, predicate abstraction, theoretical computer science, program analysis, state space, programming language, computer science, spurious relationship, model checking, abstract interpretation, algorithm, and counterexample. The authors 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.