معرفی
Sandrine Blazy is a Professor at the University of Rennes, where she teaches mechanized semantics (in Coq), functional programming (in OCaml), formal methods (using Why3), and software vulnerabilities. She is a member of the CELTIQUE and Epicure project-teams, both affiliated with Inria Rennes and IRISA laboratory. Her research focuses on formal verification of compilers and program transformations, notably through the CompCert compiler and Versaco static analyzer.
- Education: HDR (Habilitation à Diriger des Recherches) in Computer Science, Université d'Évry Val d'Essonne (2008).
Research Interests: Her work ensures mathematical guarantees in compiler correctness, preventing security bugs during program translation. She specializes in deductive verification, static analysis, and software security, with applications in critical systems like avionics and cryptography.
Scientific Awards:
- CNRS Silver Medal (2023)
- Lucas Award from Formal Methods Europe (2023)
- ACM SIGPLAN Programming Languages Software Award (2022)
- ACM Software System Award (2021)
- Best Paper Award at FMTea 2014
- La Recherche Award in Information Sciences (2011)
Advising and Grants: She has advised numerous PhD students (e.g., Solène Mirliaz, Aurèle Barrière) and led research projects like Scrypt (secure compilation for cryptography), ERC VESTA (verified static analysis), and VERASCO (formal verification of compilers). Her grants include ANR and FNRAE funding.
Labs and Teams: Actively involved in IRISA CNRS UMR 6074 as deputy director (2021), and collaborates with Inria Rennes and CNRS project teams.
