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: