Questions: Counterexample-Guided Abstraction Refinement

Question 1

What is a spurious counterexample in the CEGAR framework?

• A. A counterexample that is too long to be useful for debugging
• B. A counterexample found in the abstract model that does not correspond to any feasible execution in the concrete system — it is an artifact of over-approximation
• C. A counterexample that violates a safety property but not a liveness property
• D. A counterexample generated by a faulty model checker

Answer: (B)

Abstraction over-approximates the concrete system: it includes all real behaviors but may also include behaviors that are not actually possible. A spurious counterexample is a trace that exists in the abstract model but cannot be replayed in the concrete system because the abstraction lost a critical distinction. For example, if the abstraction merges two variable values that the program keeps separate, it might exhibit a path that the real program can never take. CEGAR refines the abstraction to separate these merged values.

Question 2

CEGAR always terminates.

• T. True
• F. False

Answer: False

CEGAR is not guaranteed to terminate in general. Each refinement step eliminates the current spurious counterexample, but the number of refinements needed could be unbounded (though in practice it is usually small). For finite-state systems with finite abstractions, termination is guaranteed because there are finitely many possible refinements. For infinite-state systems or when using predicate abstraction, the set of possible predicates is infinite and termination depends on the specific system and property. Many practical CEGAR implementations terminate quickly, but theoretical guarantees are limited.

Question 3

Explain the three main steps of a CEGAR iteration and what happens at each step.

Model answer: 1. Abstract and model-check: build an abstract model and check the property. If the property holds, the system is verified (abstraction is a safe over-approximation). 2. Check counterexample feasibility: if the model checker finds a counterexample in the abstract model, simulate it on the concrete system to determine if it is real. 3. Refine or report: if the counterexample is real, report the bug. If spurious, analyze WHY it is infeasible, identify which concrete distinctions the abstraction must preserve, refine the abstraction accordingly, and repeat from step 1.

The elegance of CEGAR is that refinement is targeted: the spurious counterexample tells you exactly what the abstraction got wrong. In predicate abstraction, refinement adds new predicates that distinguish the states the counterexample conflated. This means the abstraction grows only as much as needed — it starts maximally coarse and gets refined only where counterexamples demand it, keeping the abstract model as small as possible.