Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Z3 Special Interest Group

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.


The program is to be determined. There will be three days of informal talks and social activities including dinners scheduled for the evenings.

When and Where

November 2 - 4, 2011
Microsoft Research
Cambridge, UK

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?

Secret Sauce

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, 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).


A PDF version of the program is available here.

Wednesday, November 2

9.00 Welcome & Breakfast
9.30 Tony Hoare


The Verified Software Initiative


Hillel Kugler


Z3 for Biology
10.30 Break
11.00 The Z3 Team


New and future features of Z3 Slides 1 Slides 2
12.00 Lunch
13.30 Adrien Champion


Assumptio and Stuff: using Z3 in a collaborative parallel formal verification framework. Slides


Marko Kääramees


Symbolic analysis of EFSM models for test generation using Z3 Slides


Juhan Ernits


Application of Z3 in Consistency Based Diagnosis of Hybrid Systems and Beyond
15.00 Break
15.30 Malte Schwerhoff


Comparing Verification Condition Generation with Symbolic Execution Slides


Joseph N. Ruskiewicz


Using Debuggers to Understand Failed Verification Attempts


Arlen Cox
Counterexample Generation for Separation Logic Slides
17.00 Close
18.00 Coach to pick up attendees from MSRC
19.00 Evening Dinner at Restaurant Alimentum


Thursday, November 3

9.00 Welcome & Breakfast
9.30 Byron Cook
Symbolic software model checking with Z3
Andrey Rybalchenko
Towards Automatic Synthesis of Software Verification Tools
10.30 Break
11.00 Nik Sultana
Solving trust issues using Z3 Slides
Alexander Malkis
Automatic verification of software barriers: Z3 vs. MONA vs. BAPA.
12.00 Lunch
13.30 Chantal Keller
Certification of SMT proof witnesses in the Coq proof assistant Slides
Tjark Weber
Independent Proof Reconstruction for Z3: An Overview
Sascha Boehme
Proof Automation for Isabelle via Z3
15.00 Break
15.30 Jasmin Blanchette
Sledgehammer with Z3 Makes Isabelle Happy
Konstantin Korovin and Christoph Sticksel
Z3 for iProver-Eq: efficient ground solving for instantiation-based first-order reasoning Slides
  Philippe Suter
  Programming with Z3
17.00 Close
19.00 Evening Dinner at Corpus Christi College


Friday, November 4


Welcome & Breakfast
9.30 Carsten Fuhs
Automated Termination Analysis for Programming Languages via Non-Linear SMT and Term Rewriting
Silvio Ranise
Symbolic Backward Reachability with Effectively Propositional Logic
10.30 Break
11.00 Paul Jackson
Proving SPARK-Ada verification conditions using SMT solvers
Margus Veanes
Microsoft.Automata library: application to Bek
12.00 Lunch
13.30 Swen Jacobs
SMT-based Reactive Synthesis
Marek Trtik
Overapproximating Program Paths using FOL Formula Slides
Maria Paola Bonacina
Towards an interpolating DPLL(Gamma+T) Slides
15.00 Break
15.30 Vladimir Klebanov
Theory reasoning in deductive program verification Slides
Denis Nicole
The ESBMC model checker for multi-threaded C
17.00 Close
19.00 Pub crawl
Leonardo de Moura
Leonardo de Moura

Nikolaj Bjorner
Nikolaj Bjorner

Youssef Hamadi
Youssef Hamadi