Sciweavers

Share
CADE
2002
Springer

Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

9 years 10 months ago
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.
Harald Rueß, Leonardo Mendonça de Mou
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2002
Where CADE
Authors Harald Rueß, Leonardo Mendonça de Moura, Maria Sorea
Comments (0)
books