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 Rocq 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 Rocq) 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
I am the general chair for POPL 2026,
which will be held in Rennes.
Submit a paper! Attend the meeting!
News
- [10/24] Invited talk: "Some challenges and work in progress in verified compilation of realistic languages", Big specification programme, Newton Institute, Cambridge, United Kingdom
- [06/24] Lecturer on compiler verification at the summer school on modelling and verification of parallel processes
- [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/23] Lecturer on compiler verification at the Oregon Programming Languages and Verification Technology, Systems & Applications summer schools
- [06/23] Invited talk: How to provide proof that software is bug-free? Verified compilation to the rescue National days of GDR GPL
- [03/23] Award: I am deeply honored to receive the 2023 CNRS Silver Medal
- [03/23] 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/23] 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/23] Invited talk: CompCert: a journey through the landscape of mechanized semantics for verified compilation, CPP 2023 conference
- [07/22] Invited talk on CompCert, annual meeting of the WG VERIF of the GDR IM
- [05/22] 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/22] Invited talk: Obfuscation du logiciel : brouiller le code pour protger les programmes, sminaire du cours Scurit du logiciel : quel rle pour les langages de programmation ?, Collge de France
- [03/22] Invited talk: Semantic preservation of constant-time policies during compilation, Annual meeting of the WG formal methods for security of the GDR scurit
- [09/21] Invited talk: A tutorial on teaching deductive verification with Why3, Tutorial Series of the FME Teaching Committee
Recent program committees
- ICFP 2025, CPP 2025 (co-chair), PriSC 2025, ProLaLa 2024, FMTea 2024,
- CPP 2024 (co-chair), AFADL 2023, ITP 2023, FMTea 2023, ESOP 2023, FM 2023,
- Types 2022, ECOOP 2022, ITP 2022, JFLA 2022, POPL 2022, ESOP 2021
How to contact me
E-mail: Sandrine.Blazy [at] irisa.fr
Postal mail: IRISA, Campus de Beaulieu, 35 042 Rennes
cedex, France.