I am a professor in the computer science department of the University of Rennes.
I am a member of Epicure, a joint project-team with Inria and 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 C compiler. A prime application domain is software security.
I am a member of the editorial board of the LMCS journal.
I am deputy director of IRISA CNRS UMR 6074 laboratory since 2021.
I teach mechanized semantics (in Coq) and deductive verification (using Why3).
Former member of Section 6 of the national committee for scientific research CoNRS (2016-21)
Former coordinator of the LTP (Languages, Types, Proofs) group of the French GDR GPL
News
- [04/24] Invited talk: From operational semantics to verified compilation ETAPS unifying speaker, Luxembourg
- [04/24] Invited talk: 30 years as an academic ETAPS mentoring workshop, Luxembourg
- [07 and 08/2023] Lecturer on compiler verification at the Oregon Programming Languages and Verification Technology, Systems & Applications summer schools
- [06/2023] Invited talk: How to provide proof that software is bug-free? Verified compilation to the rescue National days of GDR GPL
- [03/2023] Award: I am deeply honored to receive the 2023 CNRS Silver Medal
- [03/2023] Award: I am deeply honored to receive the 2023 Lucas Award from Formal Methods Europe, along with Zaynah Dargaye and Xavier Leroy, for a highly influential paper published at the FM 2006 conference
- [01/2023] Award: I am deeply honored to receive the 2022 ACM SIGPLAN Programming Languages Software Award for the development of the CompCert formally-verified compiler, along with Xavier Leroy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan
- [01/2023] Invited talk: CompCert: a journey through the landscape of mechanized semantics for verified compilation, CPP 2023 conference
- [09/2022] Invited talk: Compilation vérifiée: vers du logiciel zéro défaut, conférence Sciences du logiciel: de l'idée au binaire CNRS
- [07/2022] Invited talk on CompCert, annual meeting of the WG VERIF of the GDR IM
- [05/2022] Award: I am deeply honored to receive the 2021 ACM Software System Award for the development of the CompCert formally-verified compiler, along with Xavier Leroy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan
- [04/2022] Invited talk: Obfuscation du logiciel : brouiller le code pour protéger les programmes, séminaire du cours Sécurité du logiciel : quel rôle pour les langages de programmation ?, Collège de France
- [03/2022] Invited talk: Semantic preservation of constant-time policies during compilation, Annual meeting of the WG formal methods for security of the GDR sécurité
- [09/2021] Invited talk: A tutorial on teaching deductive verification with Why3, Tutorial Series of the FME Teaching Committee
- [11/2020] Invited talk: From Verified Compilation to Secure Compilation: a Semantic Approach, ACM SIGSAC PLAS 2020 workshop
- [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
- [12/2018] Invited talk: Semantics preservation of program obfuscations, GDR Sécurité, Paris Saclay
- [07/2016] Logic and Semantics Seminar, Cambridge, United Kingdom
- [08/2015] Coq tutorial, ITP conference, Nanjing, China
- [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] Programming Languages Mentoring Workshop, PLMW 2015, India
- [08/2014] NII Shonan summer school on Coq, Japan
- [06/2014] Dagstuhl seminar: Challenges in Analysing Executables: Scalability, Self-Modifying Code and Synergy
- [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, VSTTE 2013 conference, Menlo Park, USA
Recent program committees
- CPP 2024 (co-chair), AFADL 2023, ITP 2023, FMTea 2023, ESOP 2023, FM 2023,
- AFADL 2022, Types 2022, ECOOP 2022, ITP 2022, JFLA 2022, POPL 2022,
- FMTea 2021, AFADL 2021, Types 2021, ESOP 2021, GPCE 2020, AFADL 2020, TyDe 2020,
- ICFP 2020 (ERC), 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
Main research projects
- ERC VESTA: verified static analysis platform (2018-2021) led by David Pichardie
- Scrypt (funded by grant ANR-18-CE25-0014): secure compilation for cryptography (2019-2022)
- 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)
How to contact me
E-mail: Sandrine.Blazy [at] irisa.fr
Postal mail: IRISA, Campus de Beaulieu, 35 042 Rennes
cedex, France.