Sandrine Blazy

77 papers A* 2A 6B 19C 6Journal 24Unranked 18

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	A Mechanized Semantics for Dataflow Circuits. Proc. ACM Program. Lang. Tony Law, Delphine Demange, Sandrine Blazy
2025	C	`conf`	Abstract machines and small-step semantics: a winning ticket for proof automation? PPDP Alain Delaët, Sandrine Blazy, Denis Merigoux
2025	—	`conf`	Formal Verification of WTO-based Dataflow Solvers - Artifact Experience Report. ESOP (2) Roméo La Spina, Delphine Demange, Sandrine Blazy
2025	—	`conf`	Formal Verification of WTO-based Dataflow Solvers. ESOP (2) Roméo La Spina, Delphine Demange, Sandrine Blazy
2025	B	`ed.`	Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025 CPP Kathrin Stark, Amin Timany, Sandrine Blazy, Nicolas Tabareau
2024	B	`conf`	From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert. FASE Sandrine Blazy
2024	B	`ed.`	Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024 CPP Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy
2023	B	`conf`	CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). CPP Sandrine Blazy
2023	J	`jnl`	Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. Proc. ACM Program. Lang. Aurèle Barrière, Sandrine Blazy, David Pichardie
2023	B	`conf`	Mechanised Semantics for Gated Static Single Assignment. CPP Yann Herklotz, Delphine Demange, Sandrine Blazy
2022	J	`jnl`	Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert Backend into a Formally Verified JIT Compiler. CoRR Aurèle Barrière, Sandrine Blazy, David Pichardie
2021	J	`jnl`	Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek
2021	A	`conf`	Secure Compilation of Constant-Resource Programs. CSF Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie
2020	—	`conf`	A Fast Verified Liveness Analysis in SSA Form. IJCAR (2) Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie
2020	J	`jnl`	Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2020	—	`conf`	From Verified Compilation to Secure Compilation: a Semantic Approach. PLAS@CCS Sandrine Blazy
2019	J	`jnl`	A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. J. Autom. Reason. Frédéric Besson, Sandrine Blazy, Pierre Wilke
2019	J	`jnl`	CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. J. Autom. Reason. Frédéric Besson, Sandrine Blazy, Pierre Wilke
2019	A	`conf`	Compiling Sandboxes: Formally Verified Software Fault Isolation. ESOP Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke
2019	J	`jnl`	Formal Verification of a Constant-Time Preserving C Compiler. IACR Cryptol. ePrint Arch. Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2019	B	`conf`	Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. CPP Sandrine Blazy, Rémi Hutin
2019	—	`conf`	Teaching Deductive Verification in Why3 to Undergraduate Students. FMTea Sandrine Blazy
2019	J	`jnl`	Verifying constant-time implementations by abstract interpretation. J. Comput. Secur. Sandrine Blazy, David Pichardie, Alix Trieu
2018	J	`jnl`	Selected Extended Papers of VSTTE 2016. J. Autom. Reason. Sandrine Blazy, Marsha Chechik
2017	B	`conf`	CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. ITP Frédéric Besson, Sandrine Blazy, Pierre Wilke
2017	B	`conf`	Structuring Abstract Interpreters Through State and Value Abstractions. VMCAI Sandrine Blazy, David Bühler, Boris Yakobowski
2017	A	`conf`	Verified Translation Validation of Static Analyses. CSF Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu
2017	—	`conf`	Verifying Constant-Time Implementations by Abstract Interpretation. ESORICS (1) Sandrine Blazy, David Pichardie, Alix Trieu
2016	A	`conf`	An abstract memory functor for verified C static analyzers. ICFP Sandrine Blazy, Vincent Laporte, David Pichardie
2016	B	`conf`	Formal verification of control-flow graph flattening. CPP Sandrine Blazy, Alix Trieu
2016	J	`jnl`	Improving static analyses of C programs with conditional predicates. Sci. Comput. Program. Sandrine Blazy, David Bühler, Boris Yakobowski
2016	J	`jnl`	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. J. Autom. Reason. Sandrine Blazy, Vincent Laporte, David Pichardie
2016	—	`ed.`	Verified Software. Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17-18, 2016, Revised Selected Papers VSTTE Sandrine Blazy, Marsha Chechik
2015	B	`conf`	A Concrete Memory Model for CompCert. ITP Frédéric Besson, Sandrine Blazy, Pierre Wilke
2015	A*	`conf`	A Formally-Verified C Static Analyzer. POPL Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
2015	C	`conf`	Data tainting and obfuscation: Improving plausibility of incorrect taint. SCAM Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent
2015	—	`conf`	Formal verification of compilers and static analyzers. PLMW@POPL Sandrine Blazy
2015	B	`ed.`	Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings SAS Sandrine Blazy, Thomas P. Jensen
2015	B	`conf`	Validating Dominator Trees for a Fast, Verified Dominance Test. ITP Sandrine Blazy, Delphine Demange, David Pichardie
2015	B	`conf`	Verified Validation of Program Slicing. CPP Sandrine Blazy, André Maroneze, David Pichardie
2014	—	`conf`	A Formally Verified WCET Estimation Tool. WCET André Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut
2014	B	`conf`	A Precise and Abstract Memory Model for C Using Symbolic Values. APLAS Frédéric Besson, Sandrine Blazy, Pierre Wilke
2014	C	`conf`	Improving Static Analyses of C Programs with Conditional Predicates. FMICS Sandrine Blazy, David Bühler, Boris Yakobowski
2014	—	`conf`	Measuring the robustness of source program obfuscation: studying the impact of compiler optimizations on the obfuscation of C programs. CODASPY Sandrine Blazy, Stéphanie Riaud
2014	B	`conf`	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. ITP Sandrine Blazy, Vincent Laporte, David Pichardie
2013	—	`conf`	Formal Verification of Loop Bound Estimation for WCET Analysis. VSTTE Sandrine Blazy, André Maroneze, David Pichardie
2013	J	`jnl`	Formal Verification of a C Value Analysis Based on Abstract Interpretation CoRR Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
2013	B	`conf`	Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
2013	B	`ed.`	Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings ITP Sandrine Blazy, Christine Paulin-Mohring, David Pichardie
2013	C	`conf`	Proofs you can believe in: proving equivalences between Prolog semantics in Coq. PPDP Jael Kriener, Andy King, Sandrine Blazy
2011	J	`jnl`	Introduction. Tech. Sci. Informatiques Sandrine Blazy
2010	A	`conf`	Formal Verification of Coalescing Graph-Coloring Register Allocation. ESOP Sandrine Blazy, Benoît Robillard, Andrew W. Appel
2009	B	`conf`	Live-range unsplitting for faster optimal coalescing. LCTES Sandrine Blazy, Benoît Robillard
2009	J	`jnl`	Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reason. Sandrine Blazy, Xavier Leroy
2009	J	`jnl`	Mechanized semantics for the Clight subset of the C language CoRR Sandrine Blazy, Xavier Leroy
2008	J	`jnl`	Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. Autom. Reason. Xavier Leroy, Sandrine Blazy
2008	—	`book`	Sémantiques formelles. (Formal semantics). Sandrine Blazy
2007	J	`jnl`	Chronique : Comment gagner la confiance en C? Tech. Sci. Informatiques Sandrine Blazy
2007	—	`conf`	Separation Logic for Small-Step cminor. TPHOLs Andrew W. Appel, Sandrine Blazy
2007	J	`jnl`	Separation Logic for Small-step Cminor CoRR Andrew W. Appel, Sandrine Blazy
2006	B	`conf`	Formal Verification of a C Compiler Front-End. FM Sandrine Blazy, Zaynah Dargaye, Xavier Leroy
2006	J	`jnl`	Partial Evaluation for Program Comprehension CoRR Sandrine Blazy
2006	J	`jnl`	Reuse of Specification Patterns with the B Method CoRR Sandrine Blazy, Frédéric Gervais, Régine Laleau
2005	C	`conf`	Formal Verification of a Memory Model for ICFEM Sandrine Blazy, Xavier Leroy
2003	—	`conf`	Reuse of Specification Patterns with the B Method. ZB Sandrine Blazy, Frédéric Gervais, Régine Laleau
2000	J	`jnl`	Specifying and Automatically Generating a Specialization Tool for Fortran 90. Autom. Softw. Eng. Sandrine Blazy
1998	J	`jnl`	Partial Evaluation for Program Comprehension. ACM Comput. Surv. Sandrine Blazy, Philippe Facon
1997	A*	`conf`	Application of Formal Methods to the Development of a Software Maintenance Tool. ASE Sandrine Blazy, Philippe Facon
1996	—	`conf`	An Automatic Interprocedural Analysis for the Understanding of Scientific Application Programs. Dagstuhl Seminar on Partial Evaluation Sandrine Blazy, Philippe Facon
1996	—	`conf`	Interprocedural analysis for program comprehension by specialization. WPC Sandrine Blazy, Philippe Facon
1995	—	`conf`	Formal Specification and Prototyping of a Program Specializer. TAPSOFT Sandrine Blazy, Philippe Facon
1994	J	`jnl`	Partial Evaluation for the Understanding of Fortran Programs. Int. J. Softw. Eng. Knowl. Eng. Sandrine Blazy, Philippe Facon
1994	—	`conf`	SFAC, a tool for program comprehension by specialization. WPC Sandrine Blazy, Philippe Facon
1993	A	`conf`	Partial Evaluation and Symbolic Computation for the Understanding of Fortran Programs CAiSE Sandrine Blazy, Philippe Facon
1993	C	`conf`	Partial Evaluation for the Understanding of FORTRAN Programs. SEKE Sandrine Blazy, Philippe Facon
1993	—	`conf`	Partial evaluation as an aid to the comprehension of Fortran programs. WPC Sandrine Blazy, Philippe Facon
1992	—	`conf`	Software maintenance: an analysis of industrial needs and constraints. ICSM Marc Haziza, J. F. Voidrot, E. Minor, L. Pofelski, Sandrine Blazy