Sandrine Blazy

I am professor in the computer science department (ISTIC) of the University of Rennes 1.

I am a member of CELTIQUE, a joint project-team with INRIA Rennes Bretagne Atlantique and the IRISA CNRS 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 C compiler and the Verasco static analyzer. A prime application domain is software security.

I teach mechanized semantics (in Coq), functional programming, formal methods (using the Why3 tool), and software vulnerabilities.

Member of Section 6 of the national committee for scientific research CoNRS from Sept. 2016.

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

Previously in charge of the M2 SSI graduate curriculum dedicated to information system security (2009-2013), and of the research master in computer science (2013-2017).

[09/2019] Invited talk: Formal Verification of a Constant-Time Preserving C Compiler, Verified software workshop, Newton institute, Cambridge, United Kingdom

[05/2019] Effective Verification: Static Analysis Meets Program Logics, Lorentz center, Netherlands

[04/2019] IFIP WG 2.11 meeting, Boston, USA

[12/2018] Invited talk: Semantics preservation of program obfuscations, GDR Sécurité, Paris Saclay

[07/2018] IFIP WG 1.9/2.15 meeting, Oxford, United Kingdom

[06/2018] IFIP WG 2.11 meeting, Kyoto, Japan

[05/2018] Talk given at the University of Utah, USA

[10/2017] Annual meeting of the LTP French community, Paris

[05/2017] IFIP WG 1.9/2.15 meeting, Leuven, Belgium

[08/2016] IFIP WG 2.11 meeting, Bloomington, USA

[07/2016] Logic and Semantics Seminar, Cambridge, United Kingdom

[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

POPL 2020, PriSC 2020, APLAS 2019, SpISA 2019, ITP 2019, AFADL 2019,

LOPSTR 2018, ICFP 2018, AFADL 2018, EuroS&P 2018, CPP 2018, IFL 2017,

SRC@PLDI 2017, TFP 2017, GPCE 2017, VSTTE 2017, AFADL 2017, CoqPL 2017 (co-chair),

PLMW@SPLASH 2016 (co-chair), APLAS 2016, IFL 2016,

VSTTE 2016 (co-chair), GPCE'16, DS@STAF16, AFADL 2016, CPP 2016,

SAS 2015 (co-chair), OCaml workshop 2015, ITP 2015, AFADL 2015,

VSTTE 2014, AFADL 2014, CC 2014, LPAR 2013, ITP 2013 (co-chair), VMCAI 2013

Teaching Deductive Verification in Why3 to Undergraduate Students. FMTea 2019

Compiling Sandboxes: Formally Verified Software Fault Isolation, with Frédéric Besson, Alexandre Dang, Thomas Jensen and Pierre Wilke. ESOP 2019

Formal verification of a program obfuscation based on mixed boolean-arithmetic expressions, with Rémi Hutin. CPP 2019

L'assistant de preuve Coq, with Pierre Castéran and Hugo Herbelin. Techniques de l'Ingénieur, 2017

Verified Constant-Time Implementations by Abstract Interpretation, with David Pichardie and Alix Trieu. ESORICS 2017

CompCertS: a memory-aware verified C compiler using pointer as integer semantics, with Frédéric Besson and Pierre Wilke. ITP 2017

Verified Translation Validation of Static Analyses, with Gilles Barthe, Vincent Laporte, David Pichardie and Alix Trieu. CSF 2017

Structuring Abstract Interpreters Through State and Value Abstractions, with David Bühler and Boris Yakobowski. VMCAI 2017

An Abstract Memory Functor for Verified C Static Analyzers, with Vincent Laporte and David Pichardie. ICFP 2016

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. CPP 2016

Data tainting and Obfuscation: Improving Plausibility of Incorrect Taint, with Stéphanie Riaud and Thomas Sirvent. SCAM 2015

Validating Dominator Trees for a Fast, Verified Dominance Test, with Delphine Demange and David Pichardie. ITP 2015

A concrete memory model for CompCert, with Frédéric Besson and Pierre Wilke. ITP 2015

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

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

A Precise and Abstract Memory Model for C using Symbolic Values, with Frédéric Besson and Pierre Wilke. APLAS 2014

Improving Static Analyses of C Programs with Conditional Predicates, with David Bühler and Boris Yakobowski. FMICS 2014. Best paper award.

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code, with Vincent Laporte and David Pichardie. 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. PPDP 2013 .

Formal Verification of Loop Bound Estimation for WCET Analysis, with Andre Maroneze and David Pichardie. VSTTE 2013 .

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

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