Abstract: The Satisfiability Modulo Theories (SMT) problem is that of checking the satisfiability of first-order formulas with respect to some logical theory T of interest. This talk will briefly review the theoretical framework for SMT and then discuss some of the main issues involved in creating a practical implementation, in particular, the need for and implementation of fast Boolean reasoning. The talk will also cover the implementation of non-convex theories and strategies for quantifier instantiation in the context of SMT.

Clark Barrett received his bachelor's degree in Mathematics, Computer Science, and Electrical Engineering from Brigham Young University in 1995. He received his PhD from Stanford University and joined the faculty of New York University in the Fall of 2002. Professor Barrett is the co-author of a number of SMT systems, including the Stanford Validity Checker (SVC), and its successor, the Cooperating Validity Checker (CVC). His current research includes work on a new version of CVC, called CVC3, as well as applications of CVC3 to hardware and software verification. Appointments: dcm@cs.cmu.edu