-
Separation logic in Coq.
Separation logic meeting, 13 juillet 2008, Université de Princeton.
-
Vérification formelle d'un modèle mémoire pour le langage C.
Séminaire LSL du CEA-LIST, 18 mars 2008, CEA Saclay.
-
Vérification formelle d'un front-end pour un compilateur C.
Journée du PPF Logiciels sûrs, 7 juin 2007, CNAM.
-
Programmation en nombres entiers et compilation certifiée.
Journée CEDRIC, 30 janvier 2007, CNAM.
-
Une logique de séparation pour Cminor.
Séminaire PPS, 14 décembre 2006, Université Paris 7.
- Une sémantique de C pour un compilateur certifié en Coq.
Séminaire LOGICAL-PROVAL, 14 octobre 2005, LRI, Université d'Orsay.