-
Vérification formelle
de compilateurs optimisants pour logiciel embarqué.
Comité scientifique sectoriel STIC, 14 mai 2009, ANR, Paris.
-
Vérification formelle d'un compilateur C.
24 mars 2009, LABRI, Bordeaux.
-
Vérification formelle
d'un compilateur C.
Séminaire 68NQRT, 6 mars 2009, IRISA, Rennes.
-
Vérification formelle d'un compilateur C: un tutoriel (avec Xavier Leroy).
24 février 2009, Airbus, Toulouse.
-
Sémantiques formelles pour un compilateur certifié du langage C.
Séminaire LIFO, 5 janvier 2009, Université d'Orléans, Orléans.
-
Un parcours de la compilation certifiée à la preuve de programmes.
Séminaire LACL, 8 décembre 2008, Université Paris 12, Créteil.
-
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.