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.
