General Theorem Proving for Satisfiability Modulo Theories: An Overview

Опубликовано 6 сентября 2016, 17:22

Program analysis and verification require decision procedures for satisfiability modulo theories (SMT),that decides the satisfiability, or, dually, the validity, of formulae in decidable fragments of specific theories or combinations thereof. Examples include the quantifier-free fragments of theories of data structures such as lists, arrays and records. The challenge is to have decision procedures that are simultaneously sound, complete, expressive and efficient, to handle problems of practical interest without incurring in false negatives or false positives. Theorem proving by deduction mechanisms like resolution and rewriting is concerned with the general validity problem in first-order logic with equality, which is only semi-decidable. However, if a deduction mechanism is proved to terminate on a class of SMT problems, it yields a decision procedure. Furthermore, problems from applications may require to drop restrictions such as quantifier-free so that general theorem proving comes into play. This talk will give an overview of our results in applying general theorem proving to the design of decision procedures for SMT, including: Rewrite-based satisfiability procedures for several theories of data structures, including instances of polynomial complexity, a generic approach to combinations of theories, and a decomposition method where the theorem prover is applied to compile part of the problem for an SMT-solver, so that the complementary strengths of first-order theorem provers and SMT-solvers may be combined.