Sandrine Blazy

Depuis 2003, d'abord dans le cadre de l'ARC Concert, puis 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.

Formal Verification of Coalescing Graph-Coloring Register Allocation, avec Benoît Robillard et Andrew Appel. Actes de la conférence ESOP 2010.

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. October 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.

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.

• ASCERT: (founded by FNRAE) vérification formelle d'analyses statiques (2009-2012)
• U3CAT: (financé par l'ANR) unification de techniques d'analyse de code C critique dans la plateforme Frama-C (2008-2011).
• CompCert: (financé par l'ANR) vérification formelle d'un compilateur optimisant du langage C(2005-2007)

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

GPG public key