Bounded Model Checking and Induction: From Refutation to Verification

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.

Proceedings of the 15th Computer-Aided Verification conference (CAV). Lecture Notes in Computer Science. Springer-Verlag, 2003. © Springer-Verlag.

gzipped postscript or postscript

BibTeX Entry

@InProceedings{dMRS:cav03,
  author =       "Leonardo de Moura and Harald Rue{\ss} and Maria
                 Sorea",
  title =        "Bounded Model Checking and Induction: From Refutation to Verification",
  editor =       "Andrei Voronkov",
  booktitle =    "Computer-Aided Verification, CAV 2003",
  year =         "2003",
  series =       "Lecture Notes in Computer Science",
  volume =       "2725",
  publisher =    "Springer-Verlag",
  pages =        "14--26"
}