ENabling TRust through Os Proofs... and beYond
25-26 Jan 2018 Villeneuve d'Ascq (France)

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 DamKTH 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 RepublicUruguay
 
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
 
Online user: 1