Induction in CEGAR for Detecting Counterexamples

Induction has been studied in model checking for proving the validity of safety properties, i.e., showing the absence of counterexamples. To our knowledge, induction has not been used to refute safety properties. Existing algorithms including bounded model checking, predicate abstraction, and interpolation are not efficient in detecting long counterexamples. In this paper, we propose the use of induction inside the counterexample guided abstraction and refinement (CEGAR) loop to prove the existence of counterexamples. We target bugs whose counterexamples are long and yet can be captured by regular patterns. We identify the pattern algorithmically by analyzing the sequence of spurious counterexamples generated in the CEGAR loop, and perform the induction proof automatically. The new method has little additional overhead to CEGAR and this overhead is insensitive to the actual length of the concrete counterexample.