Developing Efficient SMT Solvers
                               Leonardo de Moura
                               One Microsoft Way
                                 Redmond, WA
                                   98052 USA


                                      Abstract
    Decision procedures for checking satisfiability of logical formulas are crucial for
many verification applications. Of particular recent interest are solvers for Satisfia-
bility Modulo Theories (SMT). SMT solvers decide logical satisfiability (or dually,
validity) of formulas in classical multi-sorted first-order logic with equality, with
respect to a background theory. The success of SMT for verification applications
is largely due to the suitability of supported background theories for expressing
verification conditions.
    In this talk I will discuss how modern SMT solvers work, and the main im-
plementation techniques used. I will also describe how SMT solvers are used in
industry and Microsoft in particular.