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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
De Moura, L., Rueß, H., & Sorea, M. (2003). Bounded model checking and induction: From refutation to verification (extended abstract, category A). Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2725, 14–26. https://doi.org/10.1007/978-3-540-45069-6_2
Mendeley helps you to discover research relevant for your work.