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