I am professor in the computer science department (ISTIC) of the University of Rennes 1. I am in charge of the research master in computer science. Previously, I was 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. In 2012 and 2013, I was scientific director of the language and software engineering department of IRISA.

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 mechanized semantics (in Coq), functional programming (in OCaml), formal methods (using the Why3 tool), and software vulnerabilities.

I am coordinator of the LTP (Languages, Types, Proofs) group of the French GDR GPL. This group is funded by CNRS and meets twice a year in a French city.

Events

[05/2016] Cost EUtypes meeting, Novi Sad, Serbia

[01/2016] IFIP WG 1.9/2.15 meeting, Saint-Petersburg, USA

[11/2015] IFIP WG 2.11 meeting, London

[10/2015] Annual meeting of the LTP French community, Nancy

[08/2015] Coq tutorial, ITP conference, Nanjing, China

[07/2015] IFIP WG 1.9/2.15 meeting, Menlo Park, USA

[04/2015] Dagstuhl seminar: Qualification of formal methods tools, Germany

[03/2015] NII Shonan meeting on low-level code analysis and applications to computer security, Japan

[01/2015] Invited talk: Formal verification of static analysis, IFIP WG 2.11, Stellenbosch, South Africa

[01/2015] Programming Languages Mentoring Workshop, PLMW 2015, India

[12/2014] Invited talk: A precise and abstract memory model for C using symbolic values, IFIP WG 1.9/2.15, Paris

[08/2014] NII Shonan summer school on Coq, Japan

[07/2014] Invited talk: Formal verification of a static analyzer based on abstract interpretation, IFIP WG 1.9/2.15, Vienna, Austria

[06/2014] Dagstuhl seminar: Challenges in Analysing Executables: Scalability, Self-Modifying Code and Synergy, Germany

[03/2014] Invited talk: Compiling avionics software with a formally verified compiler, IFIP WG 2.11, Pittsburgh, USA

[01/2014] Invited talk (in French): Formal verification of a graph coloring algorithm for register allocation, JFLA 2014 (session in honor of JFLA's 25th birthday), previously published in JFLA 2008

[05/2013] A tutorial on the CompCert verified compiler, invited talk given at the VSTTE 2013 conference, Menlo Park, USA

[07/2012] 4th Asian-Pacific summer school on formal methods, East China Normal University, Shanghai, China

[06/2012] Annual meeting of the GDR GPL French community, Rennes

[04/2012] Podcast (in French): À propos des compilateurs.

[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

Recent program committees

Recent publications

CompCert - A formally verified optimizing compiler, with Xavier Leroy, Daniel Kästner, Bernhard Schommer, Markus Pister and Christian Ferdinand. ERTS2 2016

Formal verification of control flow flattening, with Alix Trieu. Certified Proofs and Programs, CPP 2016

Data tainting and Obfuscation: Improving Plausibility of Incorrect Taint, with Stéphanie Riaud and Thomas Sirvent. Conference on Source Code Analysis and Manipulation, SCAM 2015

Validating Dominator Trees for a Fast, Verified Dominance Test, with Delphine Demange and David Pichardie. Conference on Interactive Theorem Proving, ITP 2015

A concrete memory model for CompCert, with Frédéric Besson and Pierre Wilke. Conference on Interactive Theorem Proving, ITP 2015

A formally-verified C static analyzer, with Jacques-Henri Jourdan, Vincent Laporte, Xavier Leroy and David Pichardie. Symposium on Principles on Programming Languages, POPL 2015

Verified validation of program slicing, with André Maroneze and David Pichardie. Certified Proofs and Programs, CPP 2015

A Precise and Abstract Memory Model for C using Symbolic Values, with Frédéric Besson and Pierre Wilke. Asian Symp. on Programming Languages and Systems, APLAS 2014

Improving Static Analyses of C Programs with Conditional Predicates, with David Bühler and Boris Yakobowski. Formal Methods for Industrial Critical Systems, FMICS 2014.
Best paper award.

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code, with Vincent Laporte and David Pichardie. Interactive Theorem Proving, ITP 2014.

A Formally Verified WCET Estimation Tool, with André Maroneze, David Pichardie and Isabelle Puaut. WCET 2014

The CompCert memory model, with Xavier Leroy, Andrew Appel, Gordon Stewart. In Program Logics for Certified Compilers. Cambridge University Press. 2014.

Proofs you can believe in - Proving equivalences between Prolog semantics in Coq, with Jael Kriener and Andy King. Symposium on Principles and Practice of Declarative Programming, PPDP 2013.

Formal Verification of Loop Bound Estimation for WCET Analysis, with Andre Maroneze and David Pichardie. VSTTE - Verified Software: Theories, Tools and Experiments, VSTTE 2013.

Formal Verification of a C Value Analysis Based on Abstract Interpretation, with Vincent Laporte, Andre Maroneze and David Pichardie. Static Analysis Symposium, SAS 2013.

Towards a formally verified obfuscating compiler, with Roberto Giacobazzi. Software Security and Protection workshop, SSP 2012.

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.

Main research projects

AnaStaSec (funded by grant ANR-14-CE28-0014): static analysis for security properties (2015-2017)

BINSEC (funded by grant ANR-12-INSE-002): binary code analysis for security (2013-2016)

VERASCO (funded by grant ANR-11-INSE-003): formal verification of static analyzers and of compilers (2012-2015)

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

U3CAT (funded by ANR-08-SEGI-021): 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