Trends and Challenges in
                   Satisfiability Modulo Theories

                                         Cesare Tinelli⋆
                                  Department of Computer Science
                                      The University of Iowa
                                      tinelli@cs.uiowa.edu



Abstract
Satisfiability Modulo Theories (SMT) is concerned with the problem of deter-
mining the satisfiability of first-order formulas with respect to a given logical
theory T . A distinguishing feature of SMT is the use of inference methods tai-
lored to the particular theory T . By being theory-specific and restricting their
language to certain classes of formulas (such as, typically but not exclusively,
ground formulas), such methods can be implemented into solvers that are more
efficient in practice than general-purpose theorem provers. SMT techniques have
been traditionally developed to support deductive software verification, but they
have also applications in model checking, certifying compilers, automated test
generation, and other formal methods.
     This talk gives an overview of SMT and its applications, and highlights
some long-standing challenges for a wider applications of SMT techniques within
formal methods, as well as some fresh challenges introduced by new potential
uses. A major challenge is providing adequate model generation features for
disproving verification conditions.




⋆
    The author’s research described in this talk was made possible with the partial support of grants
    #0237422 and #0551646 from the National Science Foundation and a grant from Intel Corporation.