Orchestrating Decision Engines

Relatore:  Leonardo de Moura - Microsoft Research, Redmond
  giovedì 1 settembre 2011 alle ore 16.45 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 - Piramide, Piano 0, Sala Verde

Maria Paola Bonacina

Data pubblicazione
27 luglio 2011

Offerta formativa