Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

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