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.

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

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

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.

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.

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

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.

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.