Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)

ABSTRACT. Typical CEGAR-based verification methods refine the abstraction domain based on full traces. The finite-state model checking algorithm IC3 introduced the concept of discovering, generalizing from, and thereby eliminating individual state (or cube) counterexamples to induction (CTIs). This focus on individual states (or cubes) suggests a simpler abstraction-refinement scheme in which refinements are performed relative to single steps of the transition relation, thus reducing the expense of a refinement and eliminating the need for full traces. Interestingly, this change in refinement focus leads to a natural spectrum of refinement options, including when to refine and which type of concrete single-step query to refine relative to. Experiments validate that CTI-focused abstraction refinement, or CTIGAR, is competitive with existing CEGAR-based tools.