The school will cover four aspects of software verification:
- SMT solvers, by Pascal Fontaine (LORIA)
- Program verification with F*, by Cătălin Hriţcu (Inria Paris)
- Bounded model-checking, by Gennaro Parlato (University of Southampton)
- Concurrent program logics, by Viktor Vafeiadis (MPI Kaiserslautern)
Each topic will be covered through a long course of six hours. In addition, the school will feature four one-hour talks on more specific issues:
- SMT, String and Security by Philipp Rümmer (Uppsala University)
- Verification of invariants for convergent replicated data types by Gustavo Petri (Université Paris Diderot)
- Traces, interpolants, and automata : Ultimate Automizer’s approach to software verification by Matthias Heizmann (University of Freiburg)
- Security verification and cryptographic modelling in F*, Antoine Delignat-Lavaud (Miscrosoft Research Cambridge)
The detailed schedule of all lectures and talks is available. A rough overview (slightly misleading) is shown below. Participants are expected to arrive on Sunday evening and leave Friday afternoon (travel information).
| Mon | Tue | Wed | Thu | Fri | |
|---|---|---|---|---|---|
| AM | SMT 1 | F★ 1 | BMC 1 | BMC 2 | CPL 2 |
| PM | SMT 2 | F★ 2 | Excursion | CPL 1 |