Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

We investigate the combination of propositional SAT checkers with domain-specific theorem provers as the foundation for efficient 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 purely propositional approximations of Boolean constraint formulas are iteratively refined by generating lemmas on demand from an automated analysis of spurious counterexamples using theorem proving. We examplify bounded model checking for timed automata and for RTL level descriptions, and investigate the lazy integration of SAT solving and theorem proving.

Proceedings of the 18th International Conference on Automated Deduction (CADE '02), Lecture Notes in Computer Science, Springer-Verlag, 2002. © Springer-Verlag.

gzipped postscript or postscript

BibTeX Entry

@InProceedings{dMRS02,
  author = 	 {Leonardo de Moura and Harald Rue{\ss} and Maria Sorea},
  title = 	 {Lazy Theorem Proving for Bounded Model Checking over 
                  Infinite Domains},
  booktitle = 	 {18th Conference on Automated Deduction (CADE)},
  year =	  2002,
  series =	 {Lecture Notes in Computer Science},
  address =	 {Copenhagen, Denmark},
  month =	 {July 27-30},
  publisher =	 {Springer Verlag}
}