This program is tentative and subject to change.

Mon 16 Jan 2023 09:00 - 10:30 at Scollay - Tutorials 1A
Mon 16 Jan 2023 11:00 - 12:30 at Scollay - Tutorials 1B

SMT solvers have nowadays become nearly ubiquitous in semantics based programming tools. They solve small logic puzzles or larger constraints useful for program analysis, verification and testing. When useful, but their internals opaque, they appear as magic wands with an air of mystery. This tutorial aims to unveil internals of Z3; establishing principles used for solving design, the art of programming solvers, and the empirics employed for integrating heuristics. The goal is to give participants an overview of the main ingredients useful for designing and implementing SMT solvers and at the same time serve as an entry guide to integrating new functionality within contemporary SMT solvers. Z3 is an SMT solver available from Microsoft Research.

This program is tentative and subject to change.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change