23 novembre 2026 à 10h30
Résumé :
CompCert est l’un des rares compilateurs réalistes ayant fait l’objet
d’une vérification formelle, et le seul pour le langage C. Il lui
manque toutefois certaines fonctionnalités (en matière de performances
et de sécurité) que l’on retrouve couramment dans d’autres
compilateurs.
Le projet Chamois vise à intégrer ces fonctionnalités à CompCert.
« Jusqu’où pouvons-nous aller en s’appuyant sur des preuves formelles ? »
Travaux en collaboration avec Sylvain Boulmé et nos étudiants (Cyril Six, Léo Gourdin, Alexandre Bérard, Benjamin Bonneau)
Salle Turquoise, 4ème étage, bât ESPRIT
français
English