Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

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 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 . This problem can be reduced to the satisfiability of Boolean constraint formulas. Our verification engine for these 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.

• Type: Conference
• Year: 2002
• Where: CADE
• Authors: Harald Rueß, Leonardo Mendonça de Moura, Maria Sorea
• Keywords: Automated Reasoning, Boolean Constraint Formulas, CADE 2002, Linear Temporal Logic, Upper Bound K