April 23rd
12:30 - 14:00
Lunch
14:30 - 15:15
Tom Henzinger.
Fine tuning the dial between model
checking and program analysis
15:15 -
16:00 Radu Iosif.
Proving Termination of Tree Manipulating Programs
16:00 -
16:30 Break
16:30 -
17:15 Viktor Kuncak
Towards Efficient Satisfiability Checking for
Boolean Algebra with Presburger Arithmetic
17:15 - 18:00
Roderick Bloem.
Property-based
Synthesis
19:00
Dinner
April 24th
09:00 -
9:45 Ricardo Sisto.
Verification
of model-based cryptographic protocol implementations
09:45 - 10:30
Judicael Courant.
Computationally sound
typing for Non-Interference:
The case of deterministic and
password-based encryption
10:30 - 11:
00 Break
11:00 -
11:45 Simon Kramer.
The Meaning of "Zero" in
Zero-Knowledge Proofs
11:45 -
12:30 Laura Kovacs.
Automated Loop Invariant Generation by Algebraic Techniques Over the
Rationals
12:30 - 14:30
Lunch
14:30
Excursion to the national parc
of Vanoise.
18:00 - 18:45
Oded Maler
Fighting the clock explosion
19:00
Dinner
April 25th
09:00 -
9:45 Deepak Kapur.
Automatic Generation of Loop
Invariants using Elimination Methods.
0 9:45 - 10:30 Andrei
Voronkov.
Encodings of
Bounded LTL Model Checking in Effectively Propositional Logic
10:30 - 11:00 Break
11:00 - 11:45
Dejan Nickovic
From real-time properties to temporal
testers: verification and synthesis
11:45 - 12:30 Holger
Hermanns
Flow faster: Efficient Decision Algorithms for Probabilistic Simulations
12:30 - 14:30 Lunch