Sciweavers

FMCAD
2007
Springer

Induction in CEGAR for Detecting Counterexamples

14 years 6 months ago
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 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 ion 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.
Chao Wang, Aarti Gupta, Franjo Ivancic
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FMCAD
Authors Chao Wang, Aarti Gupta, Franjo Ivancic
Comments (0)