Sandrine Blazy

Publication Activity (10 Years)

Years Active: 1992-2024
Publications (10 Years): 32

Top Topics

Formal Verification

Abstract Interpretation

Graduate Students

Fault Isolation

Top Venues

J. Autom. Reason.

Proc. ACM Program. Lang.

Publications

Sandrine Blazy
From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert. FASE (2024)
Yann Herklotz, Delphine Demange, Sandrine Blazy
Mechanised Semantics for Gated Static Single Assignment. CPP (2023)
Aurèle Barrière, Sandrine Blazy, David Pichardie
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. Proc. ACM Program. Lang. 7 (POPL) (2023)
Sandrine Blazy
CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). CPP (2023)
Aurèle Barrière, Sandrine Blazy, David Pichardie
Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert Backend into a Formally Verified JIT Compiler. CoRR (2022)
Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie
Secure Compilation of Constant-Resource Programs. CSF (2021)
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek
Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. 5 (POPL) (2021)
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4 (POPL) (2020)
Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie
A Fast Verified Liveness Analysis in SSA Form. IJCAR (2) (2020)
Sandrine Blazy
From Verified Compilation to Secure Compilation: a Semantic Approach. PLAS@CCS (2020)
Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke
Compiling Sandboxes: Formally Verified Software Fault Isolation. ESOP (2019)
Sandrine Blazy
Teaching Deductive Verification in Why3 to Undergraduate Students. FMTea (2019)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. J. Autom. Reason. 63 (2) (2019)
Sandrine Blazy, David Pichardie, Alix Trieu
Verifying constant-time implementations by abstract interpretation. J. Comput. Secur. 27 (1) (2019)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. J. Autom. Reason. 62 (4) (2019)
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Formal Verification of a Constant-Time Preserving C Compiler. IACR Cryptol. ePrint Arch. 2019 (2019)
Sandrine Blazy, Rémi Hutin
Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. CPP (2019)
Sandrine Blazy, Marsha Chechik
Selected Extended Papers of VSTTE 2016. J. Autom. Reason. 60 (3) (2018)
Sandrine Blazy, David Bühler, Boris Yakobowski
Structuring Abstract Interpreters Through State and Value Abstractions. VMCAI (2017)
Sandrine Blazy, David Pichardie, Alix Trieu
Verifying Constant-Time Implementations by Abstract Interpretation. ESORICS (1) (2017)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. ITP (2017)
Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu
Verified Translation Validation of Static Analyses. CSF (2017)
Sandrine Blazy, David Bühler, Boris Yakobowski
Improving static analyses of C programs with conditional predicates. Sci. Comput. Program. 118 (2016)
Sandrine Blazy, Alix Trieu
Formal verification of control-flow graph flattening. CPP (2016)
Sandrine Blazy, Vincent Laporte, David Pichardie
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. J. Autom. Reason. 56 (3) (2016)
Sandrine Blazy, Vincent Laporte, David Pichardie
An abstract memory functor for verified C static analyzers. ICFP (2016)
Sandrine Blazy, Delphine Demange, David Pichardie
Validating Dominator Trees for a Fast, Verified Dominance Test. ITP (2015)
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
A Formally-Verified C Static Analyzer. POPL (2015)
Sandrine Blazy
Formal verification of compilers and static analyzers. PLMW@POPL (2015)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
A Concrete Memory Model for CompCert. ITP (2015)
Sandrine Blazy, André Maroneze, David Pichardie
Verified Validation of Program Slicing. CPP (2015)
Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent
Data tainting and obfuscation: Improving plausibility of incorrect taint. SCAM (2015)
Sandrine Blazy, Stéphanie Riaud
Measuring the robustness of source program obfuscation: studying the impact of compiler optimizations on the obfuscation of C programs. CODASPY (2014)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
A Precise and Abstract Memory Model for C Using Symbolic Values. APLAS (2014)
Sandrine Blazy, David Bühler, Boris Yakobowski
Improving Static Analyses of C Programs with Conditional Predicates. FMICS (2014)
Sandrine Blazy, Vincent Laporte, David Pichardie
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. ITP (2014)
André Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut
A Formally Verified WCET Estimation Tool. WCET (2014)
Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS (2013)
Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
Formal Verification of a C Value Analysis Based on Abstract Interpretation CoRR (2013)
Jael Kriener, Andy King, Sandrine Blazy
Proofs you can believe in: proving equivalences between Prolog semantics in Coq. PPDP (2013)
Sandrine Blazy, André Maroneze, David Pichardie
Formal Verification of Loop Bound Estimation for WCET Analysis. VSTTE (2013)
Sandrine Blazy
Introduction. Tech. Sci. Informatiques 30 (4) (2011)
Sandrine Blazy, Benoît Robillard, Andrew W. Appel
Formal Verification of Coalescing Graph-Coloring Register Allocation. ESOP (2010)
Sandrine Blazy, Benoît Robillard
Live-range unsplitting for faster optimal coalescing. LCTES (2009)
Sandrine Blazy, Xavier Leroy
Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reason. 43 (3) (2009)
Sandrine Blazy, Xavier Leroy
Mechanized semantics for the Clight subset of the C language CoRR (2009)
Xavier Leroy, Sandrine Blazy
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. Autom. Reason. 41 (1) (2008)
Sandrine Blazy
Chronique : Comment gagner la confiance en C? Tech. Sci. Informatiques 26 (9) (2007)
Andrew W. Appel, Sandrine Blazy
Separation Logic for Small-step Cminor CoRR (2007)
Andrew W. Appel, Sandrine Blazy
Separation Logic for Small-Step cminor. TPHOLs (2007)
Sandrine Blazy, Frédéric Gervais, Régine Laleau
Reuse of Specification Patterns with the B Method CoRR (2006)
Sandrine Blazy
Partial Evaluation for Program Comprehension CoRR (2006)
Sandrine Blazy, Zaynah Dargaye, Xavier Leroy
Formal Verification of a C Compiler Front-End. FM (2006)
Sandrine Blazy, Xavier Leroy
-Like Imperative Languages. ICFEM (2005)
Sandrine Blazy, Frédéric Gervais, Régine Laleau
Reuse of Specification Patterns with the B Method. ZB (2003)
Sandrine Blazy
Specifying and Automatically Generating a Specialization Tool for Fortran 90. Autom. Softw. Eng. 7 (4) (2000)
Sandrine Blazy, Philippe Facon
Partial Evaluation for Program Comprehension. ACM Comput. Surv. 30 (3es) (1998)
Sandrine Blazy, Philippe Facon
Application of Formal Methods to the Development of a Software Maintenance Tool. ASE (1997)
Sandrine Blazy, Philippe Facon
Interprocedural analysis for program comprehension by specialization. WPC (1996)
Sandrine Blazy, Philippe Facon
An Automatic Interprocedural Analysis for the Understanding of Scientific Application Programs. Dagstuhl Seminar on Partial Evaluation (1996)
Sandrine Blazy, Philippe Facon
Formal Specification and Prototyping of a Program Specializer. TAPSOFT (1995)
Sandrine Blazy, Philippe Facon
SFAC, a tool for program comprehension by specialization. WPC (1994)
Sandrine Blazy, Philippe Facon
Partial Evaluation for the Understanding of Fortran Programs. Int. J. Softw. Eng. Knowl. Eng. 4 (4) (1994)
Sandrine Blazy, Philippe Facon
Partial evaluation as an aid to the comprehension of Fortran programs. WPC (1993)
Sandrine Blazy, Philippe Facon
Partial Evaluation and Symbolic Computation for the Understanding of Fortran Programs CAiSE (1993)
Sandrine Blazy, Philippe Facon
Partial Evaluation for the Understanding of FORTRAN Programs. SEKE (1993)
Marc Haziza, J. F. Voidrot, E. Minor, L. Pofelski, Sandrine Blazy
Software maintenance: an analysis of industrial needs and constraints. ICSM (1992)