Orchestrating Decision Engines

Speaker:  Leonardo de Moura - Microsoft Research, Redmond
  Thursday, September 1, 2011 at 4:45 PM 16:45 rinfresco; ore 17:00 inizio seminario

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.

Ca' Vignal 3 - Piramide, Floor 0, Hall Verde

Contact person
Maria Paola Bonacina

Publication date
July 27, 2011