Counterexample-guided Abstraction Refinement

Counterexample-guided abstraction refinement (CEGAR) is a technique for symbolic model checking. It is also applied in modal logic tableau calculi algorithms to optimise their efficiency.

In computer-aided verification and analysis of programs, models of computation often consist of states. Models for even small programs, however, may have an enormous number of states. This is identified as the state explosion problem. CEGAR addresses this problem with two stages — ''abstraction'', which simplifies a model by grouping states, and ''refinement'', which increases the precision of the abstraction to better approximate the original model.

If a desired property for a program is not satisfied in the abstract model, a counterexample is generated. The CEGAR process then checks whether the counterexample is spurious, i.e., if the counterexample also applies to the under-abstraction but not the actual program. If this is the case, it concludes that the counterexample is attributed to inadequate precision of the abstraction. Otherwise, the process finds a bug in the program. Refinement is performed when a counterexample is found to be spurious. The iterative procedure terminates either if a bug is found or when the abstraction has been refined to the extent that it is equivalent to the original model.

Program verification

Abstraction

To reason about the correctness of a program, particularly those involving the concept of time for concurrency, state transition models are used. In particular, finite-state models can be used along with temporal logic in automatic verification. The concept of abstraction is thus founded upon a mapping between two Kripke structures. Specifically, programs can be described with control-flow automata (CFA).

Define a Kripke structure $M$ as $\langle S, s_0, R, L\rangle$, where
* $S$ is a finite set of states,
* $s_0$ is an initial state in $S$,
* $R$ is a total transition relation, and
* $L$ is a function that labels each state with a set of propositional names that hold therein.

An abstraction of $M$ is defined by $\langle S_\alpha, s_0^\alpha, R_\alpha, L_\alpha \rangle$ where $\alpha$ is an abstraction mapping that maps every state in $S$ to a state in $S_\alpha$.

To preserve the critical properties of the model, the abstraction mapping maps the initial state in the original model $s_0$ to its counterpart $s_0^\alpha$ in the abstract model. The abstraction mapping also guarantees that the transition relations between two states are preserved.

Model checking

In each iteration, model checking is performed for the abstract model. Bounded model checking, for instance, generates a propositional formula that is then checked for Boolean satisfiability by a SAT solver.

Refinement

When counterexamples are found, they are examined to determine if they are spurious examples, i.e., they are unauthentic ones that emerge from the under-abstraction of the model. A non-spurious counterexample reflects the incorrectness of the program, which may be sufficient to terminate the program verification process and conclude that the program is incorrect. The main objective of the refinement process handle spurious counterexamples. It eliminates them by increasing the granularity of the abstraction.

The refinement process ensures that the dead-end states and the bad states do not belong to the same abstract state. A dead-end state is a reachable one with no outgoing transition whereas a bad-state is one with transitions causing the counterexample.

Tableau calculi

Since modal logic is often interpreted with Kripke semantics, where a Kripke frame resembles the structure of state transition systems concerned in program verification, the CEGAR technique is also implemented for automated theorem proving.

References

{{Reflist

Model checking
Logical calculi
Modal logic