Mon doctorat s'inscrit au sein du projet ANR
CompCert dont le
responsable est
Xavier Leroy.
Ce projet consiste à développer
vérifier formallement avec l'assistant à la preuve Coq un compilateur optimisant
d'un vaste sous-ensemble du langage C destiné au domaine du logiciel embarqué
critique. Le compilateur est aujourd'hui opérationnel mais continue d'être
amélioré, notamment au niveau des optimisations que celui-ci effectue. Le code
actuellement produit possède une niveau d'efficacité compris entre les niveaux
0 et 1 d'optimisation du compilateur gcc.