The Z3 Satisfiability Modulo Theories (SMT) problem solver is used in many different contexts. This meeting is an opportunity for researchers to exchange experiences with others and the developers of Z3. Participants are invited to present their applications and use of Z3. We will provide an update on new developments in Z3 as well as an assortment of social events.
Z3 in the Wild
We invite attendees to describe their uses of Z3. In particular we are interested to share experiences and to provide inspiration among users of Z3 and also extract useful challenges for Z3 and the SMT community. Describe your application. How does it invoke Z3? Which features are you using? What obstacles did you encounter? What alternatives have you considered and what are the trade-offs?
We will give a session on some of the newer features in Z3 as well as recurring themes. The topics include: Strategies, Model-based Quantifier instantiation (MBQI), Theory solvers, Real arithmetic solvers, Proof objects, Simplification, Fixed-points, Configuring Z3, Quantifier instantiation with patterns, encoding techniques (e.g., bit-vectors or integers; using algebraic data-types and arrays).
The detailed program is to be determined. There will be three days of informal talks and social activities including dinners scheduled for the evenings.
We are happy to include two keynotes form Microsoft Researchers:
- Rustan Leino — Reasoning about Programs
- Patrice Godefroid — SAGE: White-box Fuzzing using Billions and Billions of SMT constraints
There will also be an interactive session with several other Microsoft Research tools that use Z3.