Software maintenance: an analysis of industrial needs and constraints. - Marc Haziza; J. F. Voidrot; E. Minor; L. Pofelski; Sandrine Blazy (ICSM, 1992)

Partial Evaluation and Symbolic Computation for the Understanding of Fortran Programs - Sandrine Blazy; Philippe Facon (CAiSE, 1993)

Partial evaluation as an aid to the comprehension of Fortran programs. - Sandrine Blazy; Philippe Facon (WPC, 1993)

SFAC, a tool for program comprehension by specialization. - Sandrine Blazy; Philippe Facon (WPC, 1994)

Partial Evaluation for the Understanding of Fortran Programs. - Sandrine Blazy; Philippe Facon (Int. J. Softw. Eng. Knowl. Eng., 1994)

Formal Specification and Prototyping of a Program Specializer. - Sandrine Blazy; Philippe Facon (TAPSOFT, 1995)

An Automatic Interprocedural Analysis for the Understanding of Scientific Application Programs. - Sandrine Blazy; Philippe Facon (Dagstuhl Seminar on Partial Evaluation, 1996)

Interprocedural analysis for program comprehension by specialization. - Sandrine Blazy; Philippe Facon (WPC, 1996)

Application of Formal Methods to the Development of a Software Maintenance Tool. - Sandrine Blazy; Philippe Facon (ASE, 1997)

Partial Evaluation for Program Comprehension. - Sandrine Blazy; Philippe Facon (ACM Comput. Surv., 1998)

Specifying and Automatically Generating a Specialization Tool for Fortran 90. - Sandrine Blazy (Autom. Softw. Eng., 2000)

Reuse of Specification Patterns with the B Method. - Sandrine Blazy; Frédéric Gervais; Régine Laleau (ZB, 2003)

Formal Verification of a Memory Model for C-Like Imperative Languages. - Sandrine Blazy; Xavier Leroy (ICFEM, 2005)

Formal Verification of a C Compiler Front-End. - Sandrine Blazy; Zaynah Dargaye; Xavier Leroy (FM, 2006)

Partial Evaluation for Program Comprehension - Sandrine Blazy (CoRR, 2006)

Separation Logic for Small-Step cminor. - Andrew W. Appel; Sandrine Blazy (TPHOLs, 2007)

Chronique : Comment gagner la confiance en C? - Sandrine Blazy (Tech. Sci. Informatiques, 2007)

Sémantiques formelles. (Formal semantics). - Sandrine Blazy (2008)

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. - Xavier Leroy; Sandrine Blazy (J. Autom. Reason., 2008)

Live-range unsplitting for faster optimal coalescing. - Sandrine Blazy; Benoît Robillard (LCTES, 2009)

Mechanized Semantics for the Clight Subset of the C Language. - Sandrine Blazy; Xavier Leroy (J. Autom. Reason., 2009)

Formal Verification of Coalescing Graph-Coloring Register Allocation. - Sandrine Blazy; Benoît Robillard; Andrew W. Appel (ESOP, 2010)

Introduction. - Sandrine Blazy (Tech. Sci. Informatiques, 2011)

Proofs you can believe in: proving equivalences between Prolog semantics in Coq. - Jael Kriener; Andy King; Sandrine Blazy (PPDP, 2013)

Formal Verification of a C Value Analysis Based on Abstract Interpretation. - Sandrine Blazy; Vincent Laporte; André Maroneze; David Pichardie (SAS, 2013)

Formal Verification of Loop Bound Estimation for WCET Analysis. - Sandrine Blazy; André Maroneze; David Pichardie (VSTTE, 2013)

A Precise and Abstract Memory Model for C Using Symbolic Values. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (APLAS, 2014)

Measuring the robustness of source program obfuscation: studying the impact of compiler optimizations on the obfuscation of C programs. - Sandrine Blazy; Stéphanie Riaud (CODASPY, 2014)

A Formally Verified WCET Estimation Tool. - André Maroneze; Sandrine Blazy; David Pichardie; Isabelle Puaut (WCET, 2014)

Verified Validation of Program Slicing. - Sandrine Blazy; André Maroneze; David Pichardie (CPP, 2015)

A Concrete Memory Model for CompCert. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (ITP, 2015)

Validating Dominator Trees for a Fast, Verified Dominance Test. - Sandrine Blazy; Delphine Demange; David Pichardie (ITP, 2015)

Formal verification of compilers and static analyzers. - Sandrine Blazy (PLMW@POPL, 2015)

A Formally-Verified C Static Analyzer. - Jacques-Henri Jourdan; Vincent Laporte; Sandrine Blazy; Xavier Leroy; David Pichardie (POPL, 2015)

Data tainting and obfuscation: Improving plausibility of incorrect taint. - Sandrine Blazy; Stéphanie Riaud; Thomas Sirvent (SCAM, 2015)

Formal verification of control-flow graph flattening. - Sandrine Blazy; Alix Trieu (CPP, 2016)

An abstract memory functor for verified C static analyzers. - Sandrine Blazy; Vincent Laporte; David Pichardie (ICFP, 2016)

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. - Sandrine Blazy; Vincent Laporte; David Pichardie (J. Autom. Reason., 2016)

Improving static analyses of C programs with conditional predicates. - Sandrine Blazy; David Bühler; Boris Yakobowski (Sci. Comput. Program., 2016)

Verified Translation Validation of Static Analyses. - Gilles Barthe; Sandrine Blazy; Vincent Laporte; David Pichardie; Alix Trieu (CSF, 2017)

Structuring Abstract Interpreters Through State and Value Abstractions. - Sandrine Blazy; David Bühler; Boris Yakobowski (VMCAI, 2017)

Selected Extended Papers of VSTTE 2016. - Sandrine Blazy; Marsha Chechik (J. Autom. Reason., 2018)

Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. - Sandrine Blazy; Rémi Hutin (CPP, 2019)

Compiling Sandboxes: Formally Verified Software Fault Isolation. - Frédéric Besson; Sandrine Blazy; Alexandre Dang; Thomas P. Jensen; Pierre Wilke (ESOP, 2019)

Teaching Deductive Verification in Why3 to Undergraduate Students. - Sandrine Blazy (FMTea, 2019)

A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (J. Autom. Reason., 2019)

CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (J. Autom. Reason., 2019)

Verifying constant-time implementations by abstract interpretation. - Sandrine Blazy; David Pichardie; Alix Trieu (J. Comput. Secur., 2019)

A Fast Verified Liveness Analysis in SSA Form. - Jean-Christophe Léchenet; Sandrine Blazy; David Pichardie (IJCAR (2), 2020)

From Verified Compilation to Secure Compilation: a Semantic Approach. - Sandrine Blazy (PLAS@CCS, 2020)

Formal verification of a constant-time preserving C compiler. - Gilles Barthe; Sandrine Blazy; Benjamin Grégoire; Rémi Hutin; Vincent Laporte; David Pichardie; Alix Trieu (Proc. ACM Program. Lang., 2020)

Secure Compilation of Constant-Resource Programs. - Gilles Barthe; Sandrine Blazy; Rémi Hutin; David Pichardie (CSF, 2021)

Formally verified speculation and deoptimization in a JIT compiler. - Aurèle Barrière; Sandrine Blazy; Olivier Flückiger; David Pichardie; Jan Vitek (Proc. ACM Program. Lang., 2021)

Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert Backend into a Formally Verified JIT Compiler. - Aurèle Barrière; Sandrine Blazy; David Pichardie (CoRR, 2022)

CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). - Sandrine Blazy (CPP, 2023)

Mechanised Semantics for Gated Static Single Assignment. - Yann Herklotz; Delphine Demange; Sandrine Blazy (CPP, 2023)

Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. - Aurèle Barrière; Sandrine Blazy; David Pichardie (Proc. ACM Program. Lang., 2023)

From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert. - Sandrine Blazy (FASE, 2024)

Formal Verification of WTO-based Dataflow Solvers. - Roméo La Spina; Delphine Demange; Sandrine Blazy (ESOP (2), 2025)

Formal Verification of WTO-based Dataflow Solvers - Artifact Experience Report. - Roméo La Spina; Delphine Demange; Sandrine Blazy (ESOP (2), 2025)

A Mechanized Semantics for Dataflow Circuits. - Tony Law; Delphine Demange; Sandrine Blazy (Proc. ACM Program. Lang., 2025)