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 consists of states. The number of states that models even small programs, however, can be enormous — the state explosion problem emerges. CEGAR addresses this problem with two stages — abstraction, which simplifies a model by grouping states, and refinement, which increases the precision of the abstraction that closer resembles 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 for the actual program. If so, the counterexample is due to inadequate precision of the abstraction. Otherwise, the process finds a bug in the program. For a spurious counterexample, refinement is performed. 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

See also: Kripke structure

To reason about the correctness of a program, particularly those involving the concept of time for concurrency, state transition models are used. Define a Kripke structure $M$ as $\langle S,s_{0},R,L\rangle$, where

• $S$ is a finite set of states,
• $s_{0}$ a set of initial states in $S$,
• $R$ 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.

Programs can be described with control flow automata (CFA).

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 under-abstraction of the model. A non-spurious counterexample reflects 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 handles 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.