Abstract: Decision procedures for checking satisfiability of logical formulas are crucial for many verification applications. Of particular recent interest are solvers for Satisfiability 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 implementation techniques used. I will also describe how SMT solvers are used in industry and Microsoft in particular.

Leonardo de Moura is a researcher in the Software Reliability group at Microsoft Research , Redmond, WA. He obtained his Ph.D. in Computer Science from PUC-Rio in 2000. From 2001-2006, he was a Computer Scientist at SRI International. He was the main designer of the Yices SMT solver which won all divisions in the last SMT competition. Appointments: dcm@cs.cmu.edu