Sandrine Blazy

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.

Mechanized semantics for the Clight subset of the C language, avec Xavier Leroy. JAR 2009. 43(3), October 2009.

Register allocation by graph coloring under full live-range splitting, avec Benoît Robillard. Actes de la conférence LCTES 2009.

Sémantiques formelles. Habilitation à diriger des recherches. Université d'Évry Val d'Essonne. 23 octobre 2008.

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. Actes de la conférence 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.

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

E-mail: Sandrine.Blazy@irisa.fr
Snail mail: IRISA, Campus de Beaulieu, 35 042 Rennes cedex, France.
Phone: 02 99 84 22 87.