bibkey: “clarke2000counterexample” authors: “Edmund Clarke; Orna Grumberg; Somesh Jha; Yuan Lu; Helmut Veith” year: 2000 title: “Counterexample-Guided Abstraction Refinement” doi: “10.1007/10722167_15” claim: “Counterexample-guided refinement validates abstract counterexamples and refines an abstraction when they are spurious.” strata_touched: [] license: “citation-only” triage: “anchor”

Counterexample-Guided Abstraction Refinement

Verified locator

Computer Aided Verification, CAV 2000, pages 154–169. The paper treats ACTL* verification with overapproximating abstractions, checks whether an abstract counterexample is realizable, and refines after a spurious counterexample. Coarsest counterexample-eliminating refinement is NP-hard in the stated setting. This is a source for the refinement method, not for a new equality-quotient theorem or universal termination on infinite state spaces.