Abstract: The Satisfiability Modulo Theories problem is that of checking the satisfiability of first-order formulas with respect to some logical theory T of interest. What distinguishes SMT from general automated deduction is that the theory T need not be finitely (or even first-order) axiomatizable, and that specialized inference methods are used for each theory. By being theory specific and restricting their language to only certain classes of formulas, these specialized methods yield solvers that are more efficient in practice than general-purpose theorem provers. While SMT techniques have been traditionally used to support deductive software verification, they are now finding applications also in model checking and automated test generation, among others. This talk gives a two-part overview of the state of the art in SMT, focusing on general methods for increasing the scope of individual theory solvers. In particular, the first part will present methods for expanding the input language of a theory solver to more general formulas, while the second part will present methods for combining theory solvers together into solvers for richer theories.

Dr. Tinelli is an associate professor of Computer Science at the University of Iowa. His researc h interests include automated reasoning, formal methods, foundations of programming languages, and applications of logic in computer science. He co-leads an international initiative, called SMT-LIB, supported by several research groups in academia and industry, aimed at producing a number of common standards for SMT applications, as well as a large library of theories and benchmarks. He has served in the program committee of several automated reasoning conferences and workshops, and is currently a steering committee member of CADE, IJCAR, FTP, and FroCoS. Appointments: dcm@cs.cmu.edu