| Monday July 31 | Tuesday August 1 | Wednesday August 2 | Thursday August 3 | Friday August 4 | |
| 08:00 | Registration | 08:45 | Opening | ||
|---|---|---|---|---|---|
| 09:00 |
State-of-the-art SAT solving slides (solving) ⋅ code |
Practical Session on SAT/SMT | Symbolic Computation (Quantifier Elimination) slides | Cylindrical Algebraic Decomposition and Real Polynomial Constraints slides | Industrial Applications and Challenges for Verifying Reactive Embedded Software slides |
| 10:30 | Coffee break | Coffee break | Coffee break | Coffee break | Coffee break |
| 11:00 | State-of-the-art SAT solving slides (processing) | Practical Session on SAT/SMT | Symbolic Computation (Quantifier Elimination) | Cylindrical Algebraic Decomposition and Real Polynomial Constraints | Formal Verification in an Industrial Setting slides (pdf) ⋅ slides (mp4) |
| 11:45 | Closing | ||||
| 12:30 | Lunch | Lunch | Lunch | Lunch | Lunch |
| 14:00 | Foundations of Satisfiability Modulo Theories slides | State-of-the-art FOL Solving slides | Syntax-Guided Synthesis slides | Symbolic Computation through Maple and Reduce slides and worksheets | |
| 15:30 | Coffee break | Coffee break | Coffee break | Coffee break | |
| 16:00 | Foundations of Satisfiability Modulo Theories | Interactive Theorem Proving in Higher-Order Logics slides | Syntax-Guided Synthesis | Symbolic Computation through Maple and Reduce | |
| 17:30 | Break | ||||
| 17:45 | Formal Verification of Financial Algorithms | Some information on Saarland, its history, and the restaurant | |||
| 18:00 | Bus transfer to the restaurant (from MPI) | ||||
| 18:30 | |||||
| 19:00 | Get together | Dinner |