Sandrine Blazy

I am professor in the computer science department (ISTIC) of the University of Rennes 1, where I am in charge of the M2 SSI graduate curriculum dedicated to information system security.

I am a member of CELTIQUE, a joint project-team with INRIA Rennes Bretagne Atlantique and the IRISA UMR 6074 laboratory.

My research activities concern the formal verification using the Coq proof assistant of program transformations and semantic properties of programming languages, such as those found in the CompCert compiler.

I teach functional programming (in OCaml), formal methods (using the KeY tool), software testing and software vulnerabilities.

I am in charge of a seminar devoted to formal methods and security. This seminar is funded by the DGA-MI. It takes place at INRIA Rennes Bretagne Atlantique, usually in the Turing amphitheater.

[01/2012] Mechanized semantics with applications to compiler verification, lecture given at the "verifying and certifying software" winter school (ENS Lyon).

[10/2011] Along with Xavier Leroy, Zaynah Dargaye and Jean-Baptiste Tristan, I am honored to be awarded the 2011 La Recherche prize in Information Sciences for our work on the CompCert verified C compiler.

[10/2011] Annual meeting of the LTP (Languages, Types, Proofs) French community, Rennes

[08/2011] CompCert: formal verification of a realistic C compiler, lecture given at the 3rd Asian-Pacific summer school on formal methods, Suzhou, China

[04/2011] Third meeting of the French community of compilation, Dinard.

[04/2011] Mechanized semantics for compiler verification, invited talk, ACCA workshop, Chamonix.

[04/2011] TSI special issue, formal methods for static analysis and compilation (in French).

[08/2010] CompCert, a Coq certified C compiler, lecture given at the 2nd Asian-Pacific summer school on formal methods, Beijing, China

Formally verified optimizing compilation in ACG-based flight control software, with Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel and Jean Souyris, symposium ERTS2 2012.

Formal Verification of Coalescing Graph-Coloring Register Allocation, with Benoît Robillard and Andrew Appel. ESOP 2010 conference.

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

Register allocation by graph coloring under full live-range splitting, with Benoît Robillard. LCTES 2009 conference.

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, with Xavier Leroy. JAR 2008. 41(1), July 2008.

Separation Logic for Small-step C Minor, with Andrew Appel. TPHOL'07 conference, September 2007.

Experiments in validating formal semantics for C. Workshop "C/C++ verification", July 2007.

Formal verification of a C compiler front-end, with Zaynah Dargaye and Xavier Leroy. FM'06 conference, August 2006.

VERASCO (funded by ANR) (2012-2016)

ASCERT: (funded by FNRAE) formal verification of static analysis (2009-2012)

U3CAT: (funded by ANR) unification of critical C code analysis techniques inside the Frama-C platform (2008-2011).

CompCert: (funded by ANR) formal verification of a C compiler (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