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 |
Maintainer | [ Home > Seminar ] |
`Last modified: Sat Apr 21 11:09:10 EDT 2007 |