Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

---

Authors

Leonardo de Moura, Harald Rueß, and Maria Sorea

Abstract

We investigate the combination of propositional SAT checkers with domain-specific theorem provers as a foundation for bounded model checking over infinite domains. Given a program M over an infinite state type, a linear temporal logic formula phi with domain-specific constraints over program states, and an upper bound k, our procedure determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification phi. This problem can be reduced to the satisfiability of Boolean constraint formulas. Our verification engine for these kinds of formulas is lazy in that propositional abstractions of Boolean constraint formulas are incrementally refined by generating lemmas on demand from an automated analysis of spurious counterexamples using theorem proving. We exemplify bounded model checking for timed automata and for RTL level descriptions, and investigate the lazy integration of SAT solving and theorem proving.

gzipped postscript or postscript

BibTeX Entry

@inproceedings{dMRS:CADE2002,
  TITLE = {Lazy Theorem Proving for Bounded Model Checking over Infinite Domains},
  AUTHOR = {Leonardo de Moura and Harald Rue{\ss} and Maria Sorea},
  BOOKTITLE = {Proceedings of the 18th International Conference on Automated Deduction},
  YEAR = {2002},
  MONTH = {July}, 
  PUBLISHER = {Springer-Verlag}, 
  PAGES = {438--455},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2392},
  ISBN = {3-540-43931-5}
}

---

Harald Ruess: ruess@csl.sri.com