Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)

Abstract. Typical CEGAR-based verification methods refine the ab-stract domain based on full counterexample traces. The finite state model checking algorithm IC3 introduced the concept of discovering, gener-alizing from, and thereby eliminating individual state counterexamples to induction (CTIs). This focus on individual states suggests a simpler abstraction-refinement scheme in which refinements are performed rela-tive to single steps of the transition relation, thus reducing the expense of 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 ab-straction refinement, or CTIGAR, is competitive with existing CEGAR-based tools.