Accéder directement au contenu

Sandrine Blazy

78
Documents
Identifiants chercheurs

Présentation

Publications

Image document

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
Proceedings of the ACM on Programming Languages, 2023, pp.1-28. ⟨10.1145/3571202⟩
Article dans une revue hal-03882598v1
Image document

Formally verified speculation and deoptimization in a JIT compiler

Aurèle Barrière , Sandrine Blazy , Olivier Flückiger , David Pichardie , Jan Vitek
Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.26. ⟨10.1145/3434327⟩
Article dans une revue hal-03185848v1
Image document

Formal verification of a constant-time preserving C compiler

Gilles Barthe , Sandrine Blazy , Benjamin Grégoire , Rémi Hutin , Vincent Laporte
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩
Article dans une revue hal-02975012v1
Image document

Verifying constant-time implementations by abstract interpretation

Sandrine Blazy , David Pichardie , Alix Trieu
Journal of Computer Security, 2019, 27 (1), pp.137--163. ⟨10.3233/JCS-181136⟩
Article dans une revue hal-02025047v1
Image document

A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data

Frédéric Besson , Sandrine Blazy , Pierre Wilke
Journal of Automated Reasoning, 2019, 62 (4), pp.433-480. ⟨10.1007/s10817-017-9439-z⟩
Article dans une revue hal-01656895v1
Image document

CompCertS: A Memory-Aware Verified C Compiler using a Pointer as Integer Semantics

Frédéric Besson , Sandrine Blazy , Pierre Wilke
Journal of Automated Reasoning, 2019, 63 (2), pp.369-392. ⟨10.1007/s10817-018-9496-y⟩
Article dans une revue hal-02401182v1
Image document

L'Assistant de Preuve Coq Table des matières

Sandrine Blazy , Pierre Castéran , Hugo Herbelin
Techniques de l'Ingénieur, 2017
Article dans une revue hal-01645486v1
Image document

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

Sandrine Blazy , Vincent Laporte , David Pichardie
Journal of Automated Reasoning, 2016, 56 (3), pp.26. ⟨10.1007/s10817-015-9359-8⟩
Article dans une revue hal-01243700v1
Image document

Improving static analyses of C programs with conditional predicates

Sandrine Blazy , David Bühler , Boris Yakobowski
Science of Computer Programming, 2016, 118, ⟨10.1145/2854065.2854082⟩
Article dans une revue hal-01242077v1

À propos des compilateurs

Sandrine Blazy , Joanna Jongwane
Interstices, 2012
Article dans une revue hal-01350238v1
Image document

Mechanized semantics for the Clight subset of the C language

Sandrine Blazy , Xavier Leroy
Journal of Automated Reasoning, 2009, 43 (3), pp.263-288. ⟨10.1007/s10817-009-9148-3⟩
Article dans une revue inria-00352524v1
Image document

Formal verification of a C-like memory model and its uses for verifying program transformations

Xavier Leroy , Sandrine Blazy
Journal of Automated Reasoning, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩
Article dans une revue inria-00289542v1
Image document

Comment gagner confiance en C ?

Sandrine Blazy
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2007, numéro spécial "Langages applicatifs", 26 (9), pp.1195-1200. ⟨10.3166/TSI.26.1195-1200⟩
Article dans une revue inria-00292049v1
Image document

Specifying and automatically generating a specialization tool for Fortran 90

Sandrine Blazy
Automated Software Engineering, 2000, 7 (4), pp.345-376
Article dans une revue inria-00108501v1

Partial evaluation for the understanding of Fortran programs

Sandrine Blazy , Philippe Facon
International Journal of Software Engineering and Knowledge Engineering, 1994, 4, pp.535-559
Article dans une revue hal-01124467v1

Mechanised Semantics for Gated Static Single Assignment

Yann Herklotz , Delphine Demange , Sandrine Blazy
CPP 2023 - 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575681⟩
Communication dans un congrès hal-03899435v1
Image document

Secure Compilation of Constant-Resource Programs

Gilles Barthe , Sandrine Blazy , Rémi Hutin , David Pichardie
CSF 2021 - 34th IEEE Computer Security Foundations Symposium, Jun 2021, Dubrovnik, Croatia. pp.1-12
Communication dans un congrès hal-03221440v1
Image document

A Fast Verified Liveness Analysis in SSA Form

Jean-Christophe Léchenet , Sandrine Blazy , David Pichardie
IJCAR 2020- International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.324-340, ⟨10.1007/978-3-030-51054-1_19⟩
Communication dans un congrès hal-02904204v1
Image document

Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions

Sandrine Blazy , Rémi Hutin
CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Cascais, Portugal. pp.196-208, ⟨10.1145/3293880.3294103⟩
Communication dans un congrès hal-01955773v1
Image document

Compiling Sandboxes: Formally Verified Software Fault Isolation

Frédéric Besson , Sandrine Blazy , Alexandre Dang , Thomas Jensen , Pierre Wilke
ESOP 2019 - 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.499-524, ⟨10.1007/978-3-030-17184-1_18⟩
Communication dans un congrès hal-02316189v1

Teaching Deductive Verification in Why3 to Undergraduate Students

Sandrine Blazy
FM Tea (Formal Methods Teaching), Oct 2019, Porto, Portugal. pp.52-66, ⟨10.1007/978-3-030-32441-4_4⟩
Communication dans un congrès hal-02362306v1
Image document

CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler

Daniel Kästner , Jörg Barrho , Ulrich Wünsche , Marc Schlickling , Bernhard Schommer
ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems, 3AF, SEE, SIE, Jan 2018, Toulouse, France. pp.1-9
Communication dans un congrès hal-01643290v1
Image document

Verifying Constant-Time Implementations by Abstract Interpretation

Sandrine Blazy , David Pichardie , Alix Trieu
European Symposium on Research in Computer Security, Sep 2017, Oslo, Norway
Communication dans un congrès hal-01588444v1
Image document

CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics

Frédéric Besson , Sandrine Blazy , Pierre Wilke
ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. pp.81-97, ⟨10.1007/978-3-319-66107-0_6⟩
Communication dans un congrès hal-01656875v1
Image document

Verified Translation Validation of Static Analyses

Gilles Barthe , Sandrine Blazy , Vincent Laporte , David Pichardie , Alix Trieu
Computer Security Foundations Symposium, Aug 2017, Santa-Barbara, United States
Communication dans un congrès hal-01588422v1
Image document

Confusion de Type en C++: État de l'Art et Difficultés de Détection

Florent Saudel , Sandrine Blazy , Frédéric Besson
RESSI 2017 - Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information , May 2017, Grenoble/Autrans, France. pp.1-5
Communication dans un congrès hal-01656979v1
Image document

Closing the Gap – The Formally Verified Optimizing Compiler CompCert

Daniel Kästner , Xavier Leroy , Sandrine Blazy , Bernhard Schommer , Michael Schmidt
SSS'17: Safety-critical Systems Symposium 2017, Feb 2017, Bristol, United Kingdom. pp.163-180
Communication dans un congrès hal-01399482v1
Image document

CompCert - A Formally Verified Optimizing Compiler

Xavier Leroy , Sandrine Blazy , Daniel Kästner , Bernhard Schommer , Markus Pister
ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, Jan 2016, Toulouse, France
Communication dans un congrès hal-01238879v1
Image document

Formal Verification of Control-flow Graph Flattening

Sandrine Blazy , Alix Trieu
Certified Proofs and Programs (CPP 2016), Jan 2016, Saint-Petersburg, United States. pp.12, ⟨10.1145/2854065.2854082⟩
Communication dans un congrès hal-01242063v1
Image document

An Abstract Memory Functor for Verified C Static Analyzers

Sandrine Blazy , Vincent Laporte , David Pichardie
ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. pp.14, ⟨10.1145/2951913.2951937⟩
Communication dans un congrès hal-01339969v1
Image document

Data Tainting and Obfuscation: Improving Plausibility of Incorrect Taint

Sandrine Blazy , Stéphanie Riaud , Thomas Sirvent
Source Code Analysis and Manipulation (SCAM), Sep 2015, Bremen, Germany
Communication dans un congrès hal-01193286v1
Image document

A formally-verified C static analyzer

Jacques-Henri Jourdan , Vincent Laporte , Sandrine Blazy , Xavier Leroy , David Pichardie
POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩
Communication dans un congrès hal-01078386v1

Verified Validation of Program Slicing

Sandrine Blazy , Andre Maroneze , David Pichardie
CPP 2015 : Conference on Certified Programs and Proofs, 2015, Mumbai, India. pp.109-117, ⟨10.1145/2676724.2693169⟩
Communication dans un congrès hal-01110821v1
Image document

A Concrete Memory Model for CompCert

Frédéric Besson , Sandrine Blazy , Pierre Wilke
ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. pp.67-83, ⟨10.1007/978-3-319-22102-1_5⟩
Communication dans un congrès hal-01194549v1
Image document

Validating Dominator Trees for a Fast, Verified Dominance Test

Sandrine Blazy , Delphine Demange , David Pichardie
Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_6⟩
Communication dans un congrès hal-01193281v1

Formal verification of compilers and static analyzers.

Sandrine Blazy
PLMW@POPL 2015 - Programming Languages Mentoring Workshop, Jan 2015, Mumbai, India
Communication dans un congrès hal-01242094v1
Image document

Measuring the Robustness of Source Program Obfuscation - Studying the Impact of Compiler Optimizations on the Obfuscation of C Programs

Sandrine Blazy , Stéphanie Riaud
Fourth ACM Conference on Data and Application Security and Privacy - SIGSAC ACM CODASPY 2014, Mar 2014, San Antonio, United States
Communication dans un congrès hal-00927427v1

Improving static analyses of C programs with conditional predicates

Sandrine Blazy , David Bühler , Boris Yakobowski
FMICS 2014: Formal Methods for Industrial Critical Systems, Sep 2014, Florence, Italy. pp.15, ⟨10.1007/978-3-319-10702-8_10⟩
Communication dans un congrès hal-01242087v1

A Formally Verified WCET Estimation Tool

André Oliveira Maroneze , Sandrine Blazy , David Pichardie , Isabelle Puaut
14th International Workshop on Worst-Case Execution Time Analysis, Jul 2014, Madrid, Spain. ⟨10.4230/OASIcs.WCET.2014.11⟩
Communication dans un congrès hal-01087194v1
Image document

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

Sandrine Blazy , Vincent Laporte , David Pichardie
The 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. pp.128 - 143, ⟨10.1007/978-3-319-08970-6_9⟩
Communication dans un congrès hal-01102445v1
Image document

A Precise and Abstract Memory Model for C Using Symbolic Values

Frédéric Besson , Sandrine Blazy , Pierre Wilke
12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. pp.449 - 468, ⟨10.1007/978-3-319-12736-1_24⟩
Communication dans un congrès hal-01093312v1
Image document

Formal Verification of Loop Bound Estimation for WCET Analysis

Sandrine Blazy , André Maroneze , David Pichardie
VSTTE - Verified Software: Theories, Tools and Experiments, Natarajan Shankar, May 2013, Menlo Park, United States. pp.281-303
Communication dans un congrès hal-00848703v1
Image document

Formal Verification of a C Value Analysis Based on Abstract Interpretation

Sandrine Blazy , Vincent Laporte , André Maroneze , David Pichardie
SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344
Communication dans un congrès hal-00812515v1
Image document

Proofs You Can Believe In. Proving Equivalences Between Prolog Semantics in Coq

Jael Kriener , Andy King , Sandrine Blazy
15th International Symposium on Principles and Practice of Declarative Programming (PPDP), Sep 2013, Madrid, Spain. pp.37-48
Communication dans un congrès hal-00908848v1
Image document

Towards a formally verified obfuscating compiler

Sandrine Blazy , Roberto Giacobazzi
SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, ACM SIGPLAN, Jun 2012, Beijing, China
Communication dans un congrès hal-00762330v1
Image document

Formally verified optimizing compilation in ACG-based flight control software

Ricardo Bedin França , Sandrine Blazy , Denis Favre-Felix , Xavier Leroy , Marc Pantel
ERTS2 2012: Embedded Real Time Software and Systems, AAAF, SEE, Feb 2012, Toulouse, France
Communication dans un congrès hal-00653367v1
Image document

Formal Verification of Coalescing Graph-Coloring Register Allocation

Sandrine Blazy , Benoît Robillard , Andrew W. W. Appel
19th European Symposium on Programming (ESOP), Mar 2010, Paphos, Cyprus. pp.145-164
Communication dans un congrès inria-00477689v1

Live-Range Unsplitting for Faster Optimal Coalescing

Sandrine Blazy , Benoit Robillard
LCTES'09 ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems, Jan 2009, X, France. pp.70-79
Communication dans un congrès hal-01125616v1
Image document

Register allocation by graph coloring under full live-range splitting

Sandrine Blazy , Benoît Robillard
ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded systems (LCTES'2009), ACM, Jun 2009, Dublin, Ireland
Communication dans un congrès inria-00387749v1

Which C semantics to embed in the front-end of a formally verified compiler?

Sandrine Blazy
TTVSI (Tools and Techniques for Verification of System Infrastructure), Mar 2008, Oxford, United Kingdom. pp.31
Communication dans un congrès inria-00292441v1
Image document

Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe

Sandrine Blazy , Benoît Robillard , Eric Soutif
JFLA (Journées Francophones des Langages Applicatifs), INRIA, Jan 2008, Etretat, France. pp.31-46
Communication dans un congrès inria-00202713v1
Image document

Coloration avec préférences : complexité, inégalités valides et vérification formelle

Benoît Robillard , Sandrine Blazy , Eric Soutif
ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, ROADEF, Feb 2008, Clermont-Ferrand, France. pp.123-138
Communication dans un congrès inria-00260712v1

Coloration avec préférences dans les graphes triangulés

Sandrine Blazy , Benoît Robillard , Eric Soutif
Journées Graphes et algorithmes (JGA'07), Nov 2007, Paris, France. pp.32
Communication dans un congrès inria-00292045v1

Coloration avec préférences dans les graphes triangulés

Sandrine Blazy , Benoit Robillard , Eric Soutif
Journées Graphes et Algorithmes, Paris, Jan 2007, X, France. pp.32
Communication dans un congrès hal-01125410v1
Image document

Experiments in validating formal semantics for C

Sandrine Blazy
C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp.95-102
Communication dans un congrès inria-00292043v1
Image document

Separation Logic for Small-step Cminor

Andrew W. W. Appel , Sandrine Blazy
20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. pp.5-21
Communication dans un congrès inria-00165915v1
Image document

Formal Verification of a C Compiler Front-end

Sandrine Blazy , Zaynah Dargaye , Xavier Leroy
FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. pp.460-475, ⟨10.1007/11813040_31⟩
Communication dans un congrès inria-00106401v1
Image document

Formal verification of a memory model for C-like imperative languages

Sandrine Blazy , Xavier Leroy
ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. pp.280-299, ⟨10.1007/11576280⟩
Communication dans un congrès inria-00077921v1
Image document

Reuse of Specification Patterns with the B Method

Sandrine Blazy , Frédéric Gervais , Régine Laleau
ZB 2003: Formal Specification and Development in Z and B, Jun 2003, Turku, Finland, pp.40-57
Communication dans un congrès inria-00078953v1

Une démarche outillée pour spécifier formellement des patrons de conception réutilisables

Sandrine Blazy , Frédéric Gervais , Régine Laleau
Objets, Composants et Modèles dans l'ingénierie des SI, Jan 2003, X, France
Communication dans un congrès hal-01124805v1

An automatic detection of prokaryotic CoDing Sequences Combining Several Independent Methods

St?phanie Bocs , Sandrine Blazy , Claudine M?digue , Paul Glaser
Genome 2000, Paris, Jan 2000, X, France
Communication dans un congrès hal-01124664v1
Image document

Partial Evaluation for Program Comprehension

Sandrine Blazy , Philippe Facon
ACM Computing Surveys, Symposium on partial evaluation, 1998, (revue électonique)
Communication dans un congrès inria-00106403v1
Image document

Application of formal methods to the development of a software maintenance tool

Sandrine Blazy , Philippe Facon
ASE'97: The 12th IEEE Conference on Automated Software Engineering., Lowry, M. and Ledru, Y., Nov 1997, Lake Tahoe, Nevada, USA, pp.162-171
Communication dans un congrès inria-00078882v1
Image document

An automatic interprocedural analysis for the understanding of scientific application programs

Sandrine Blazy , Philippe Facon
Dagstuhl seminar on partial evaluation, Feb 1996, Saarbrucken, Germany. pp.1-16, ⟨10.1007/3-540-61580-6⟩
Communication dans un congrès inria-00165927v1

Interprocedural analysis for program comprehension by specialization

Sandrine Blazy , Philippe Facon
4th IEEE Workshop on Program Comprehension, Berlin, Jan 1996, X, France. pp.133-141
Communication dans un congrès hal-01124465v1

Formal specification and prorotyping of a program specializer

Sandrine Blazy , Philippe Facon
TAPSOFT'95, Aarhus, Jan 1995, X, France. pp.666-680
Communication dans un congrès hal-01124466v1
Image document

Formal specification and prototyping of a program specializer

Sandrine Blazy , Philippe Facon
TAPSOFT '95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE, May 1995, Aarhus, Denmark. pp.666-680, ⟨10.1007/3-540-59293-8_227⟩
Communication dans un congrès inria-00165933v1
Image document

SFAC, a tool for program comprehension by specialization

Sandrine Blazy , Philippe Facon
IEEE Third Workshop on Program Comprehension, Nov 1994, Washington D.C., United States. pp.162-167, ⟨10.1109/WPC.1994.341266⟩
Communication dans un congrès inria-00165938v1
Image document

Partial evaluation and symbolic computation for the understanding of Fortran programs

Sandrine Blazy , Philippe Facon
Advanced Information Systems Engineering 5th International Conference, CAiSE '93, 1993, Paris, France. pp.184-198, ⟨10.1007/3-540-56777-1⟩
Communication dans un congrès inria-00165950v1

Partial evaluation as an aid to the comprehension of Fortran programs

Sandrine Blazy , Philippe Facon
2nd IEEE Workshop on Program Comprehension, Capri, Italy, Jan 1993, X, France. pp.46-54
Communication dans un congrès hal-01124468v1

Evaluation partielle pour la compréhension de programmes Fortran

Sandrine Blazy , Philippe Facon
Software Engineering and its applications, Toulouse, December, Dec 1992, X, France. pp.411-417
Communication dans un congrès hal-01124469v1
Image document

Software maintenance: an analysis of industrial needs and constraints

Marc Haziza , Jean-François Voidrot , Jean-Pierre Queille , Lech Pofelski , Sandrine Blazy
IEEE Conference on Software Maintenance, IEEE, Nov 1992, Orlando, USA, France. pp.18-26, ⟨10.1109/ICSM.1992.242563⟩
Communication dans un congrès inria-00143556v1

The CompCert memory model

Xavier Leroy , Andrew W. Appel , Sandrine Blazy , Gordon Stewart
Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010
Chapitre d'ouvrage hal-00905435v1
Image document

Sémantiques formelles

Sandrine Blazy
Informatique [cs]. Université d'Evry-Val d'Essonne, 2008
HDR tel-00336576v1