Sciweavers

Share
CADE
2007
Springer

Solving Quantified Verification Conditions Using Satisfiability Modulo Theories

12 years 3 days ago
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
Abstract. First order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first order automated theorem proving (ATP) and automated theorem proving based on satisfiability modulo theories (SMT). Traditional ATP systems are designed to handle quantifiers easily, but often have difficulty reasoning with respect to theories. SMT systems, on the other hand, have built-in support for many useful theories, but have a much more difficult time with quantifiers. One clue on how to get the best of both worlds can be found in the legacy system Simplify which combines built-in theory reasoning with quantifier instantiation heuristics. Inspired by Simplify and motivated by a desire to provide a competitive alternative to ATP systems, this paper describes a methodology for reasoning about quantifiers in SMT systems. We present odology in the context of the Abstract DPLL Modulo Theories framework. Bes...
Yeting Ge, Clark Barrett, Cesare Tinelli
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Yeting Ge, Clark Barrett, Cesare Tinelli
Comments (0)
books