General Theorem Proving for Satisfiability Modulo Theories: An Overview

May 14, 2008
Maria Paola Bonacina | Dipartimento di Informatica of the Universita` degli Studi di Verona

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.

Speaker Details

Maria Paola Bonacina is a Professor of Computer Science with the Dipartimento di Informatica of the Universita` degli Studi di Verona, in Verona, Italy, since October 2002. From August 1993 through September 2002 she was on the faculty of the Department of Computer Science of the University of Iowa, first as Assistant Professor and then as Associate Professor. During her tenure at the University of Iowa she received an NSF CAREER Award and she was honored with a Dean Scholar Award by the College of Liberal Arts and Sciences. Maria Paola received a PhD in Computer Science from the State University of New York at Stony Brook in 1992, preceded by a “Dottorato di ricerca” and a “Laurea” both in Computer Science from the Universita` degli Studi di Milano, in Milano, Italy. Her research interests in computer science logic and artificial intelligence include automated reasoning, automated theorem proving, reasoning about programs, strategy analysis, distributed deduction, rewriting and declarative programming. She is serving on the board of trustees of the International Conference on Automated Deduction and on the board of directors of the Association for Automated Reasoning. At the Universita` degli Studi di Verona she was Director of Computer Science studies for three years and she is currently Dean of the Graduate School of Sciences, Engineering and Medicine.