Leonardo de Moura
Microsoft Research, USA
Model-Driven Decision Procedures for Arithmetic
Considering the theoretical hardness of SAT, the astonishing adeptness of SAT solvers when attacking practical problems has changed the way we perceive the limits of algorithmic reasoning. Modern SAT solvers are based on the idea of conflict driven clause learning (CDCL). The CDCL algorithm is a combination of an explicit backtracking search for a satisfying assignment complemented with a deduction system based on Boolean resolution. In this combination, the worst-case complexity of both components is circumvented by the components guiding and focusing each other. In this talk, we describe new procedures for nonlinear real arithmetic and linear integer arithmetic based on the CDCL algorithm. These procedures perform a backtracking search for a model, where the backtracking is powered by a novel conflict resolution procedure. Our approach takes advantage of the fact that each conflict encountered during the search is based on the current assignment and generally involves only a few constraints, a conflicting core. When in conflict, we project only the constraints from the conflicting core and explain the conflict in terms of the current model. The conflict resolution provides the usual benefits of a CDCL-style search engine, such as non-chronological backtracking and the ability to ignore irrelevant parts of the search space.
Leonardo de Moura is a principal researcher at Microsoft since 2006.
Before joining Microsoft, he was a computer scientist at SRI International.
He is interested in automated reasoning and decision procedures.
He received the Haifa Verification Conference Award in 2010.
He is the architect of the Z3 and Yices theorem provers, and the SAL model checker.
The Z3 theorem prover has been used at Microsoft to implement test-case generators, model checkers, and software verification tools.