There will be three days of informal talks and social activities including dinners scheduled for the evenings.
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
| 9.00 | 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 |