Induction in CEGAR for detecting counterexamples

Chao Wang, Aarti Gupta, Franjo Ivančić

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - Formal Methods in Computer Aided Design, FMCAD 2007
Pages77-84
Number of pages8
DOIs
StatePublished - Dec 1 2007
Externally publishedYes
EventFormal Methods in Computer Aided Design, FMCAD 2007 - Austin, TX, United States
Duration: Nov 11 2007Nov 14 2007

Publication series

NameProceedings - Formal Methods in Computer Aided Design, FMCAD 2007

Other

OtherFormal Methods in Computer Aided Design, FMCAD 2007
CountryUnited States
CityAustin, TX
Period11/11/0711/14/07

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Induction in CEGAR for detecting counterexamples'. Together they form a unique fingerprint.

Cite this