Sandrine Blazy

According to our database, Sandrine Blazy authored at least 58 papers between 1992 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert.

Sandrine Blazy

Proceedings of the Fundamental Approaches to Software Engineering, 2024

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., January, 2023

Mechanised Semantics for Gated Static Single Assignment.

Yann Herklotz, Delphine Demange, Sandrine Blazy

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote).

Sandrine Blazy

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022

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

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

Secure Compilation of Constant-Resource Programs.

Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

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

From Verified Compilation to Secure Compilation: a Semantic Approach.

Sandrine Blazy

Proceedings of the PLAS'20: Proceedings of the 15th Workshop on Programming Languages and Analysis for Security, 2020

A Fast Verified Liveness Analysis in SSA Form.

Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Verifying constant-time implementations by abstract interpretation.

Sandrine Blazy, David Pichardie, Alix Trieu

J. Comput. Secur., 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

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

Teaching Deductive Verification in Why3 to Undergraduate Students.

Sandrine Blazy

Proceedings of the Formal Methods Teaching - Third International Workshop and Tutorial, 2019

Compiling Sandboxes: Formally Verified Software Fault Isolation.

Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke

Proceedings of the Programming Languages and Systems, 2019

Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions.

Sandrine Blazy, Rémi Hutin

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Selected Extended Papers of VSTTE 2016.

Sandrine Blazy, Marsha Chechik

J. Autom. Reason., 2018

2017

Structuring Abstract Interpreters Through State and Value Abstractions.

Sandrine Blazy, David Bühler, Boris Yakobowski

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Verified Translation Validation of Static Analyses.

Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

2016

Improving static analyses of C programs with conditional predicates.

Sandrine Blazy, David Bühler, Boris Yakobowski

Sci. Comput. Program., 2016

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code.

Sandrine Blazy, Vincent Laporte, David Pichardie

J. Autom. Reason., 2016

An abstract memory functor for verified C static analyzers.

Sandrine Blazy, Vincent Laporte, David Pichardie

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Formal verification of control-flow graph flattening.

Sandrine Blazy, Alix Trieu

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015

Data tainting and obfuscation: Improving plausibility of incorrect taint.

Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent

Proceedings of the 15th IEEE International Working Conference on Source Code Analysis and Manipulation, 2015

A Formally-Verified C Static Analyzer.

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Formal verification of compilers and static analyzers.

Sandrine Blazy

Proceedings of the Programming Languages Mentoring Workshop, 2015

Validating Dominator Trees for a Fast, Verified Dominance Test.

Sandrine Blazy, Delphine Demange, David Pichardie

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

A Concrete Memory Model for CompCert.

Frédéric Besson, Sandrine Blazy, Pierre Wilke

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Verified Validation of Program Slicing.

Sandrine Blazy, André Maroneze, David Pichardie

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

A Formally Verified WCET Estimation Tool.

André Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut

Proceedings of the 14th International Workshop on Worst-Case Execution Time Analysis, 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

Proceedings of the Fourth ACM Conference on Data and Application Security and Privacy, 2014

A Precise and Abstract Memory Model for C Using Symbolic Values.

Frédéric Besson, Sandrine Blazy, Pierre Wilke

Proceedings of the Programming Languages and Systems - 12th Asian Symposium, 2014

2013

Formal Verification of Loop Bound Estimation for WCET Analysis.

Sandrine Blazy, André Maroneze, David Pichardie

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Formal Verification of a C Value Analysis Based on Abstract Interpretation.

Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie

Proceedings of the Static Analysis - 20th International Symposium, 2013

Proofs you can believe in: proving equivalences between Prolog semantics in Coq.

Jael Kriener, Andy King, Sandrine Blazy

Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, 2013

2011

Introduction.

Sandrine Blazy

Tech. Sci. Informatiques, 2011

2010

Formal Verification of Coalescing Graph-Coloring Register Allocation.

Sandrine Blazy, Benoît Robillard, Andrew W. Appel

Proceedings of the Programming Languages and Systems, 2010

2009

Mechanized Semantics for the Clight Subset of the C Language.

Sandrine Blazy, Xavier Leroy

J. Autom. Reason., 2009

Live-range unsplitting for faster optimal coalescing.

Sandrine Blazy, Benoît Robillard

Proceedings of the 2009 ACM SIGPLAN/SIGBED conference on Languages, 2009

2008

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations.

Xavier Leroy, Sandrine Blazy

J. Autom. Reason., 2008

Sémantiques formelles. (Formal semantics).

Sandrine Blazy

, 2008

2007

Chronique : Comment gagner la confiance en C?

Sandrine Blazy

Tech. Sci. Informatiques, 2007

Separation Logic for Small-Step cminor.

Andrew W. Appel, Sandrine Blazy

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

2006

Partial Evaluation for Program Comprehension

Sandrine Blazy

CoRR, 2006

Formal Verification of a C Compiler Front-End.

Sandrine Blazy, Zaynah Dargaye, Xavier Leroy

Proceedings of the FM 2006: Formal Methods, 2006

2005

Formal Verification of a Memory Model for <i>C</i>-Like Imperative Languages.

Sandrine Blazy, Xavier Leroy

Proceedings of the Formal Methods and Software Engineering, 2005

2003

Reuse of Specification Patterns with the B Method.

Sandrine Blazy, Frédéric Gervais, Régine Laleau

Proceedings of the ZB 2003: Formal Specification and Development in Z and B, 2003

2000

Specifying and Automatically Generating a Specialization Tool for Fortran 90.

Sandrine Blazy

Autom. Softw. Eng., 2000

1998

Partial Evaluation for Program Comprehension.

Sandrine Blazy, Philippe Facon

ACM Comput. Surv., 1998

1997

Application of Formal Methods to the Development of a Software Maintenance Tool.

Sandrine Blazy, Philippe Facon

Proceedings of the 1997 International Conference on Automated Software Engineering, 1997

1996

Interprocedural analysis for program comprehension by specialization.

Sandrine Blazy, Philippe Facon

Proceedings of the 4th International Workshop on Program Comprehension (WPC '96), 1996

An Automatic Interprocedural Analysis for the Understanding of Scientific Application Programs.

Sandrine Blazy, Philippe Facon

Proceedings of the Partial Evaluation, International Seminar, 1996

1995

Formal Specification and Prototyping of a Program Specializer.

Sandrine Blazy, Philippe Facon

Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

1994

Partial Evaluation for the Understanding of Fortran Programs.

Sandrine Blazy, Philippe Facon

Int. J. Softw. Eng. Knowl. Eng., 1994

SFAC, a tool for program comprehension by specialization.

Sandrine Blazy, Philippe Facon

Proceedings of the Proceedings 1994 IEEE 3rd Workshop on Program Comprehension, 1994

1993

Partial evaluation as an aid to the comprehension of Fortran programs.

Sandrine Blazy, Philippe Facon

Proceedings of the IEEE Second Workshop on Program Comprehension, 1993

Partial Evaluation and Symbolic Computation for the Understanding of Fortran Programs

Sandrine Blazy, Philippe Facon

Proceedings of the Advanced Information Systems Engineering, 1993

1992

Software maintenance: an analysis of industrial needs and constraints.

Marc Haziza, J. F. Voidrot, E. Minor, L. Pofelski, Sandrine Blazy

Proceedings of the Conference on Software Maintenance, 1992