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

Program (Tentative)

Thursday 25 January

08:30 - 09:00 registration
 
09:00 - 10:00 The Pip Protokernel
  David Nowak, Narjes Jomaa 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
  Zhong Shao, Yale University, United States
 
11:30 - 12:30 TBA
  June Andronick, Data61/NICTA, Australia
 
12:30 - 14:00 Lunch
 
14:00 - 15:00 The PROSPER project: Verified hypervisors at KTH
  Mads DamKTH Royal Institute of Technology, Sweden
 
15:00 - 16:00 The Semantics Stack of the Verisoft XT Project
  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
  Magnus Myreen, Chalmers University of Technology, Sweden
 
17:30 - 18:30 Debugging Debug Informations
  Francesco Zappa Nardelli, Inria, France
 

Friday 26 January

09:00 - 10:00 TBA
  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
  Adam Chlipala, MIT, United States
 
11:45 - 13:00 How to Use Formal Proofs to Detect Bugs (tentative title)
  Alexandre Miquel, University of the RepublicUruguay
 
13:00 - 14:30 Lunch
 
14:30 - 15:45 TBA
  David Cock, ETH Zurich, Switzerland
 
15:45 - 16:15 Coffee Break
 
16:15 - 17:30 Specifications: The Next Verification Bottleneck
  Alastair Reid, Arm Ltd, United Kingdom
 
17:30 - 18:00 Final Discussion / Panel
 
Online user: 1