nucleation

LIT-1652: Counterexample-Guided Abstraction Refinement

1 min read

Properties6
StatusActive — read in full 2026-10-27 (NOTE-1231), from the authors' manuscript of the CAV paper in CMU's repository; worth reading as the founding paper of counterexample-guided abstraction refinement and as an exact case of a failure under a fixed specification read as a missing distinction, located and repaired by a split. The specification itself is never revised. Two of its four theorems have no proof in this text.
Version2
Tagslogic, mathematics
Cited as “grounds” byCLAIM-470 — Inquiry is a form of specification: a question fixes which differences would count as an answer, an inquiry adds the operations that make those differences accessible, and what it finds can stabilize into a specification that constrains later inquiry; so inquiry stands to its findings as a specification to its realizations, with one difference, that an inquiry can revise what an answer could be
Cited as “paper” byNOTE-1231 — Clarke, Grumberg, Jha, Lu & Veith — Counterexample-guided abstraction refinement
Cited as “source” byTHEORY-1064 — In counterexample-guided abstraction refinement, a spurious counterexample locates the distinction its abstraction lacked: walking it forward through the concrete system, the first abstract state where no concrete continuation exists merges the states the trace can reach with the states that have the transition onward, and splitting them removes the counterexample; for finite-state programs and ACTL* properties whose counterexamples are paths or loops, repeating check and split ends in a real counterexample or a proof, THEORY-1094 — In counterexample-guided abstraction refinement the property and the concrete system are fixed inputs: the property's atomic formulas help build the first abstraction and no abstraction may merge states that disagree on them, every refinement only splits classes toward the concrete state space, and a real counterexample ends the procedure; so the loop revises which of the concrete system's distinctions the model draws, never the property or the space of possible answers

Graph View

Clarke, E., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2000). Counterexample-guided abstraction refinement. In Computer Aided Verification (LNCS 1855, pp. 154–169). Springer. doi:10.1007/10722167_15.

Read in full on 2026-10-27 (NOTE-1231).

Why this is here

A16 §6 called it “the strongest formal connection” for inquiry as specification, and read luria’s DP-016 (an awkward relation discloses a missing distinction; CLAIM-419 in this record) as “the same epistemic pattern”: failure under a specification, diagnosis of the missing distinction, refinement. A16 added the limit that CEGAR refines an abstraction for a fixed property and cannot find the property misguided. It bears on CLAIM-470 and CLAIM-476.

Backlinks