Program
Thursday 25 January
| 08:30 - 09:00 |
registration |
| |
| 09:00 - 10:00 |
Formal Development of the Pip Protokernel (slides)
|
| |
Narjes Jomaa, David Nowak and Paolo Torrini, University of Lille, France |
| |
| 10:00 - 10:30 |
Coffee Break |
| |
| 10:30 - 11:30 |
CertiKOS: A Breakthrough toward Hacker-Resistant Operating Systems (slides) |
| |
Zhong Shao, Yale University, United States |
| |
| 11:30 - 12:30 |
seL4 & Family: Fast, Trustworthy, Cheap, Deployed (slides) |
| |
June Andronick, Data61/NICTA, Australia |
| |
| 12:30 - 14:00 |
Lunch |
| |
| 14:00 - 15:00 |
The PROSPER project: Verified hypervisors at KTH (slides) |
| |
Mads Dam, KTH Royal Institute of Technology, Sweden |
| |
| 15:00 - 16:00 |
The Semantics Stack of the Verisoft XT Project (slides) |
| |
Christoph Baumann, KTH Royal Institute of Technology, Sweden |
| |
| 16:00 - 16:30 |
Coffee Break |
| |
| 16:30 - 17:30 |
Verification of the GCC-Generated Binary of the seL4 Microkernel (slides) |
| |
Magnus Myreen, Chalmers University of Technology, Sweden |
| |
| 17:30 - 18:30 |
Tales from Binary Formats (slides) |
| |
Francesco Zappa Nardelli, Inria, France |
| |
| 20:00 - |
Dinner for invited speakers |
Friday 26 January
| 09:00 - 10:00 |
Generation of Code from Coq for Succinct Data Structures (slides) |
| |
Reynald Affeldt, AIST, Japan |
| |
| 10:00 - 10:30 |
Coffee Break |
| |
| 10:30 - 11:45 |
Raising the Level of Abstraction in Systems Programming with Fiat and Extensible, Correct-by-Construction Compilers (slides) |
| |
Adam Chlipala, MIT, United States |
| |
| 11:45 - 13:00 |
How to Use Formal Proofs to Detect Bugs (slides) |
| |
Alexandre Miquel, University of the Republic, Uruguay |
| |
| 13:00 - 14:30 |
Lunch |
| |
| 14:30 - 15:45 |
Modeling the OS/Hardware Interface with Sockeye (slides) |
| |
David Cock, ETH Zurich, Switzerland |
| |
| 15:45 - 16:15 |
Coffee Break |
| |
| 16:15 - 17:30 |
Specifications: The Next Verification Bottleneck (slides) |
| |
Alastair Reid, Arm Ltd, United Kingdom |
| |
| 17:30 - 18:00 |
Final Discussion |
| |
|
