Detailed programme – EPIT 2018 Software Verification Spring School

The detailed schedule for EPIT 2018 lectures and talks follows. Beware that slight changes are still possible.

All breaks (and cocktail) are taking place at the bar, below the restaurant.

Dinner takes place everyday at 19:30.

Wine is included with dinner. Lunch includes a coffee, served at the bar. Other orders at the bar must be paid directly by participants.

9:00—10:30	SMT (Pascal Fontaine)
10:30—10:45	coffee break
10:45—12:15	SMT (Pascal Fontaine)
12:15—13:45	lunch
13:45—15:00	SMT (Pascal Fontaine)
15:00—15:15	coffee break
15:15—16:45	F* (Cătălin Hriţcu) A Gentle Introduction to F*: Verifying purely functional programs
16:45—17:00	coffee break
17:00—18:00	Traces, interpolants, and automata : Ultimate Automizer’s approach to software verification (Matthias Heizmann)
19:00—19:30	welcome cocktail

9:00—10:30	SMT (Pascal Fontaine)
10:30—10:45	coffee break
10:45—12:15	F* (Cătălin Hriţcu): Verifying Stateful Programs in F*
12:15—13:45	lunch
13:45—15:00	F* (Danel Ahman): Monotonic State in F*
15:00—15:30	coffee break
15:30—16:30	F* (Cătălin Hriţcu): F*’s effects, tactics, WPs, and SMT encoding
16:30—16:45	coffee break
16:45—18:00	Security verification and cryptographic modelling in F* (Antoine Delignat-Lavaud)

9:30—10:30	SMT, String and Security (Philipp Rümmer)
10:30—10:45	coffee break
10:45—12:15	BMC (Gennaro Parlato)
12:15—13:45	lunch
13:45—15:00	CPL (Viktor Vafeiadis)
15:00—15:15	coffee break
15:15—16:45	CPL (Viktor Vafeiadis)
16:45—17:00	coffee break
17:00—18:00	Verification of invariants for convergent replicated data type (Gustavo Petri)