| 2025 | ESOP | Formal Verification of WTO-based Dataflow Solvers. | Romo La Spina, Delphine Demange, Sandrine Blazy |
| 2025 | ESOP | Formal Verification of WTO-based Dataflow Solvers - Artifact Experience Report. | Romo La Spina, Delphine Demange, Sandrine Blazy |
| 2025 | PPDP | Abstract machines and small-step semantics: a winning ticket for proof automation? | Alain Delat, Sandrine Blazy, Denis Merigoux |
| 2024 | FASE | From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert. | Sandrine Blazy |
| 2023 | CPP | CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). | Sandrine Blazy |
| 2023 | CPP | Mechanised Semantics for Gated Static Single Assignment. | Yann Herklotz, Delphine Demange, Sandrine Blazy |
| 2020 | CADE | A Fast Verified Liveness Analysis in SSA Form. | Jean-Christophe Lchenet, Sandrine Blazy, David Pichardie |
| 2020 | CCS | From Verified Compilation to Secure Compilation: a Semantic Approach. | Sandrine Blazy |
| 2019 | CPP | Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. | Sandrine Blazy, Rmi Hutin |
| 2019 | ESOP | Compiling Sandboxes: Formally Verified Software Fault Isolation. | Frdric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke |
| 2017 | ESORICS | Verifying Constant-Time Implementations by Abstract Interpretation. | Sandrine Blazy, David Pichardie, Alix Trieu |
| 2017 | ITP | CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. | Frdric Besson, Sandrine Blazy, Pierre Wilke |
| 2017 | VMCAI | Structuring Abstract Interpreters Through State and Value Abstractions. | Sandrine Blazy, David Bhler, Boris Yakobowski |
| 2016 | CPP | Formal verification of control-flow graph flattening. | Sandrine Blazy, Alix Trieu |
| 2016 | ICFP | An abstract memory functor for verified C static analyzers. | Sandrine Blazy, Vincent Laporte, David Pichardie |
| 2015 | CPP | Verified Validation of Program Slicing. | Sandrine Blazy, Andr Maroneze, David Pichardie |
| 2015 | ITP | A Concrete Memory Model for CompCert. | Frdric Besson, Sandrine Blazy, Pierre Wilke |
| 2015 | ITP | Validating Dominator Trees for a Fast, Verified Dominance Test. | Sandrine Blazy, Delphine Demange, David Pichardie |
| 2015 | POPL | Formal verification of compilers and static analyzers. | Sandrine Blazy |
| 2015 | POPL | A Formally-Verified C Static Analyzer. | Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie |
| 2015 | SCAM | Data tainting and obfuscation: Improving plausibility of incorrect taint. | Sandrine Blazy, Stphanie Riaud, Thomas Sirvent |
| 2014 | APLAS | A Precise and Abstract Memory Model for C Using Symbolic Values. | Frdric Besson, Sandrine Blazy, Pierre Wilke |
| 2014 | FMICS | Improving Static Analyses of C Programs with Conditional Predicates. | Sandrine Blazy, David Bhler, Boris Yakobowski |
| 2014 | ITP | Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. | Sandrine Blazy, Vincent Laporte, David Pichardie |
| 2013 | PPDP | Proofs you can believe in: proving equivalences between Prolog semantics in Coq. | Jael Kriener, Andy King, Sandrine Blazy |
| 2013 | SAS | Formal Verification of a C Value Analysis Based on Abstract Interpretation. | Sandrine Blazy, Vincent Laporte, Andr Maroneze, David Pichardie |
| 2010 | ESOP | Formal Verification of Coalescing Graph-Coloring Register Allocation. | Sandrine Blazy, Benot Robillard, Andrew W. Appel |
| 2006 | FM | Formal Verification of a C Compiler Front-End. | Sandrine Blazy, Zaynah Dargaye, Xavier Leroy |
| 2005 | ICFEM | Formal Verification of a Memory Model for | Sandrine Blazy, Xavier Leroy |
| 1993 | CaiSE | Partial Evaluation and Symbolic Computation for the Understanding of Fortran Programs | Sandrine Blazy, Philippe Facon |
| 1993 | SEKE | Partial Evaluation for the Understanding of FORTRAN Programs. | Sandrine Blazy, Philippe Facon |