Bounded Model Checking and Induction: From Refutation to Verification

In: Proceedings of Computer-Aided Verification, CAV '2003.
Authors
Leonardo de Moura, Harald Rueß, Maria Sorea
Abstract
We explore the combination of bounded model checking and induction for proving safety properties of infinite-state systems. In particular, we define a general k-induction scheme and prove completeness thereof. A main characteristic of our methodology is that strengthened invariants are generated from failed k-induction proofs. This strengthening step requires quantifier-elimination, and we propose a lazy quantifier-elimination procedure, which delays expensive computations of disjunctive normal forms when possible. The effectiveness of induction based on bounded model checking and invariant strengthening is demonstrated using infinite-state systems ranging from communication protocols to timed automata and (linear) hybrid automata.
Download: PS, PDF
BibTeX Entry 
@inproceedings{dMRS:03,
  TITLE = {Bounded Model Checking and Induction: From Refutation to Verification},
  AUTHOR = {Leonardo de Moura and Harald Rue{\ss} and Maria Sorea},
  BOOKTITLE = "Proceedings of the 15th Computer-Aided Verification conference (CAV'03)",
  SERIES="LNCS",
  VOLUME=2725,
  YEAR=2003
}
Leonardo de Moura: demoura@csl.sri.com