Orchestrating Decision Engines

Leonardo de Moura - Microsoft Research, Redmond
Date and time
Thursday, September 1, 2011 at 4:45 PM - 16:45 rinfresco; ore 17:00 inizio seminario
Ca' Vignal - Piramide, Floor 0, Hall Verde
Programme Director
Maria Paola Bonacina
External reference
Publication date
July 27, 2011
Computer Science  


Constraint satisfaction problems arise in many diverse areas including
software and hardware verification, type inference, static program
analysis, test-case generation, scheduling, planning and graph
problems. These areas share a common trait, they include a
core component using logical formulas for describing states and
transformations between them. In a nutshell, symbolic logic is the
calculus of computation.
The Satisfiability Modulo Theories (SMT) solver, Z3, developed at
Microsoft Research,
can be used to check the satisfiability of logical formulas over one or
more theories.
SMT solvers offer a compelling match for software tools, since several
common software constructs map directly into supported theories.
Z3 comprises of a collection of symbolic reasoning engines. These
engines are combined to address the requirements of each application
domain. In this talk, we describe the main challenges in orchestrating
the different engines, and the main application domains within Microsoft.

© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234