Bruno Blanchet
Ecole Normale Supérieure de Paris
France
Talk: Mechanizing Game-Based Proofs of Security Protocols (abstract/
slides)
|
Hubert Comon-Lundh
Ecole Normale Supérieure de Cachan
France
Talk: Formal Security Proofs (abstract
/
slides)
|
Javier Esparza
Technische Universität München
Germany
Talk: Automata-theoretic Models of Software (
abstract
/
slides)
|
Orna Grumberg
TECHNION, Israel Institute of Technology
Israel
Talk: Model Checking (abstract
/ slides)
Exercises:
(exercise)
|
Gerwin Klein
The University of New South Wales, Sydney
Australia
Talk: Interactive Proof: Applications to Semantics (abstract
/
slides)
Material: (material)
Exercises: (exercise)
|
Marta Kwiatkowska
Oxford University
United Kingdom
Talk: Advances in Probabilistic Model Checking (abstract)
|
Rustan Leino
Microsoft Research, Redmond
USA
Talk: Using and Building an Automatic Program Verifier (abstract
/
slides)
Exercises:
(Cubes
/
Cubes, recursive
/
McCarthy
/
Coincidence
/
Saddleback search
/
Max
/
Reverse-Reverse
/
List
/
RockBand
/
C Gauss into Boogie
/
Java swap
/
FindZero translation errors)
|
Rupak Majumdar
Max Planck Institute for Software Systems, Kaiserslautern
Germany
Talk: Software Model Checking (abstract)
|
Sharad Malik
Princeton University
USA
Talk: Boolean Satisfiability Solvers: Techniques and Extensions (abstract
/
slides)
Exercises: (exercise / solution)
|
Tobias Nipkow
Technische Universität München
Germany
Talk: Interactive Proof: Hands-on Introduction (abstract
/
slides)
|
Peter O'Hearn
Queen Mary University of London
United Kingdom
Talk: Lectures on Separation Logic (abstract /
slides)
|
Andrei Sabelfeld
Chalmers University of Technology, Göteborg
Sweden
Talk: Information-Flow Security (abstract
/
slides)
|
Helmut Seidl
Technische Universität München
Germany
Talk: Precise Fixpoint Computation through Strategy Iteration and Optimization (abstract / slides)
|