Reuse of Verification Results

Conditional Model Checking, Precision Reuse, and Verification Witnesses

Dirk Beyer and Philipp Wendler

Example: Counterexample Automata

In order to present an example for a counterexample automaton that guides the verifier along a certain (error) path through a program, we use the C~program insertion_sort_false.i from the 3rd Software Verification Competition (SV-COMP'14). It implements an insertion sort algorithm and contains a bug (c.f. human-readable counterexample report produced with CPAchecker).

The counterexample automaton produced by CPAchecker after finding the bug in the program looks as follows:

Automaton in CPAchecker's textual specification format

(download)

Graphical representation produced with dot

graphical representation of error path automaton for insertion_sort_false.i
(full view)