In the last decade, advances in satisfiability-modulo-theories (SMT) solvers have powered a new generation of software tools for verification and testing. These tools transform various program analysis problems into the problem of satisfiability of formulas in propositional or first-order logic, where they are discharged by SMT solvers, such as Z3from Microsoft Research (MSR).  In this talk, I’ll review advances from MSR that expand the scope of SMT solvers on several fronts.

These advances are due to Nikolaj Bjorner, Leonardo de Moura, Ken McMillan, and Margus Veanes at MSR, and their colleagues and interns.

Tomas Ball is a Principal Researcher and Research Manager at Microsoft Research (Redmond), where he works in the area of software engineering, having made contributions in program profiling, software model checking, and empirical software engineering.  He is a 2011 ACM Fellow.