Dans cet exposé, Sandrine Blazy présente succinctement CompCert, un compilateur optimisant d'un vaste sous-ensemble de C, ayant été formellement vérifié avec l'assistant à la preuve Coq. Elle explique en particulier la propriété de préservation sémantique de ce compilateur. Ensuite, elle détaille les choix sémantiques ayant été faits pour modéliser les comportements des programmes écrits dans le langage source du compilateur, ainsi que le modèle mémoire du compilateur.
Travail réalisé en collaboration avec Xavier Leroy.
Talk
24 mars 2009 - 14h00 - 076, LaBRI
