Pierre Wilke: Formally verified compilation of low-level C code. (Compilation formellement vérifiée de code C de bas-niveau). University of Rennes 1, France 2016