Méthodes formelles pour la compilation

Travaux de recherche

Depuis 2003, d'abord dans le cadre de l'ARC Concert, puis actuellement dans le cadre du projet Compcert, je m'intéresse à l'utilisation des méthodes formelles pour spécifier et certifier un compilateur C, à l'aide de l'assistant à la preuve Coq. Cela nécessite de définir à différents niveaux d'abstraction des sémantiques formelles des langages du compilateur, et de prouver ensuite sur machine des propriétés de correction de ces sémantiques.
Dans le cadre de la thèse de Benoît Robillard, je m'intéresse également à une phase particulière de compilation, l'allocation de registres, ainsi qu'à la certification d'algorithmes d'optimisation combinatoire.
Auparavant, j'ai utilisé l'évaluation partielle dans le but de faciliter la compréhension et la maintenance d'applications scientifiques écrites en Fortran.
Dans le cadre du projet Concurrent Cminor, je m'intéresse également à la preuve de programmes impératifs fondée sur la logique de séparation.

Appel à propositions d'articles

numéro thématique de la revue TSI

Thème: APPLICATION DES MÉTHODES FORMELLES À L'ANALYSE STATIQUE ET LA COMPILATION
Date limite de soumission: 30 novembre 2008

Réunion du groupe LTP du GDR GPL

ENSIIE 28 novembre 2008

Habilitation à diriger des recherches

23 octobre 2008, 14h30, à l'ENSIIE (amphi 2)

AFADL'2009

ENSEEIHT, Toulouse, 26 - 28 janvier 2009

Publications en cours d'évaluation

Mechanized semantics for the Clight subset of the C language, avec Xavier Leroy. Soumis à un journal. Octobre 2008.

Register allocation by graph coloring under full live-range splitting, avec Benoît Robillard. Soumis à une conférence. Octobre 2008.

Publications récentes

depuis 2006

Formal verification of a C-like memory model and its uses for verifying program transformations, avec Xavier Leroy. JAR 2008. 41(1), July 2008.

Vérification formelle d'un algorithme d'allocation de registres par coloration de graphes, avec Benoît Robillard et Éric Soutif. JFLA'08, January 2008.

Separation Logic for Small-step C Minor, avec Andrew Appel. Actes de la conférence TPHOL'07, September 2007.

Experiments in validating formal semantics for C. Actes du workshop "C/C++ verification", July 2007.

Formal verification of a C compiler front-end, avec Zaynah Dargaye et Xavier Leroy. Actes de la conférence FM'06, August 2006.

Preuves en Coq

Modèle mémoire. Avec Xavier Leroy.
Compilateur Compcert (projet ANR-SSIA Compcert).
Allocation de registres. Avec Benoît Robillard.

JFLA'2008

du 26 au 29 janvier 2008

JFLA'2008 est la dix-neuvième conférence francophone organisée autour des langages applicatifs et des techniques de certification fondées sur la démonstration. Ces nouvelles journées se tiendront du 26 au 29 janvier 2008. Elles auront lieu à la mer, à Étretat.

Coordonnées

Nouvelle adresse depuis le 1er septembre 2007

E-mail: Sandrine.Blazy@ensiie.fr
Snail mail: ENSIIE, 1 square de la résistance, 91 025 Évry cedex, France.
Phone: 01 69 36 73 47. Fax: 01 69 36 73 05.