Involvement in the CertiKOS project

From 2012 to 2016, I worked in collaboration with Prof. Zhong Shao and his FLINT team at Yale University on the CertiKOS verified operating system kernel, first at Yale funded by the DARPA High-Assurance Cyber-Military Systems (HACMS) project until 2014, then starting from 2014 thanks to a partnership contract between Yale FLINT and my employer Reservoir Labs Inc. at that time, also part of (Yale FLINT's component of) the NSF DeepSpec project.

More precisely, most of my work on CertiKOS consisted in adapting the CompCert verified C compiler to support some form of verified separate compilation and stack management for CertiKOS. Thus, my work led to the following publications:

• Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro
  Certified Concurrent Abstraction Layers
  PLDI 2018
  
  
• Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu
  A Compositional Semantics for Verified Separate Compilation and Linking
  CPP 2015
  
  
• Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Xiongnan (Newman) Wu, Haozhong Zhang, Yu Guo
  Deep specifications and Certified Abstraction Layers
  POPL 2015
  
  
• Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro , Zhong Shao
  End-to-End Verification of Stack-Space Bounds for C Programs
  PLDI 2014