Sandrine Blazy

Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek. Formally verified speculation and deoptimization in a JIT compiler. Proceedings of the ACM on Programming Languages, ACM, 2021, 5, pp.26. ⟨10.1145/3434327⟩. ⟨hal-03185848⟩

Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, et al.. Formal verification of a constant-time preserving C compiler. Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩. ⟨hal-02975012⟩

Frédéric Besson, Sandrine Blazy, Pierre Wilke. CompCertS: A Memory-Aware Verified C Compiler using a Pointer as Integer Semantics. Journal of Automated Reasoning, Springer Verlag, 2019, 63 (2), pp.369-392. ⟨10.1007/s10817-018-9496-y⟩. ⟨hal-02401182⟩

Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. Journal of Automated Reasoning, Springer Verlag, 2019, 62 (4), pp.433-480. ⟨10.1007/s10817-017-9439-z⟩. ⟨hal-01656895⟩

Sandrine Blazy, David Pichardie, Alix Trieu. Verifying constant-time implementations by abstract interpretation. Journal of Computer Security, IOS Press, 2019, 27 (1), pp.137--163. ⟨10.3233/JCS-181136⟩. ⟨hal-02025047⟩

Sandrine Blazy, Pierre Castéran, Hugo Herbelin. L'Assistant de Preuve Coq Table des matières. Techniques de l'Ingenieur, Techniques de l'ingénieur, 2017. ⟨hal-01645486⟩

Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. Journal of Automated Reasoning, Springer Verlag, 2016, 56 (3), pp.26. ⟨10.1007/s10817-015-9359-8⟩. ⟨hal-01243700⟩

Sandrine Blazy, David Bühler, Boris Yakobowski. Improving static analyses of C programs with conditional predicates. Science of Computer Programming, Elsevier, 2016, 118, ⟨10.1145/2854065.2854082⟩. ⟨hal-01242077⟩

Sandrine Blazy, Joanna Jongwane. À propos des compilateurs. Interstices, INRIA, 2012. ⟨hal-01350238⟩

Sandrine Blazy, Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, Springer Verlag, 2009, 43 (3), pp.263-288. ⟨10.1007/s10817-009-9148-3⟩. ⟨inria-00352524⟩

Xavier Leroy, Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, Springer Verlag, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩. ⟨inria-00289542⟩

Sandrine Blazy. Comment gagner confiance en C ?. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2007, numéro spécial "Langages applicatifs", 26 (9), pp.1195-1200. ⟨10.3166/TSI.26.1195-1200⟩. ⟨inria-00292049⟩

Sandrine Blazy. Specifying and automatically generating a specialization tool for Fortran 90. Journal of Automated Software Engineering, Springer, 2000, 7 (4), pp.345-376. ⟨inria-00108501⟩

Sandrine Blazy, Philippe Facon. Partial evaluation for the understanding of Fortran programs. International Journal of Software Engineering and Knowledge Engineering, World Scientific Publishing, 1994, 4, pp.535-559. ⟨hal-01124467⟩

Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie. A Fast Verified Liveness Analysis in SSA Form. IJCAR 2020- International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.324-340, ⟨10.1007/978-3-030-51054-1_19⟩. ⟨hal-02904204⟩

Sandrine Blazy, Rémi Hutin. Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions. CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Cascais, Portugal. pp.196-208, ⟨10.1145/3293880.3294103⟩. ⟨hal-01955773⟩

Sandrine Blazy. Teaching Deductive Verification in Why3 to Undergraduate Students. FM Tea (Formal Methods Teaching), Oct 2019, Porto, Portugal. pp.52-66, ⟨10.1007/978-3-030-32441-4_4⟩. ⟨hal-02362306⟩

Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas Jensen, Pierre Wilke. Compiling Sandboxes: Formally Verified Software Fault Isolation. ESOP 2019 - 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.499-524, ⟨10.1007/978-3-030-17184-1_18⟩. ⟨hal-02316189⟩

Daniel Kästner, Jörg Barrho, Ulrich Wünsche, Marc Schlickling, Bernhard Schommer, et al.. CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler. ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems, 3AF, SEE, SIE, Jan 2018, Toulouse, France. pp.1-9. ⟨hal-01643290⟩

Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu. Verified Translation Validation of Static Analyses. Computer Security Foundations Symposium, Aug 2017, Santa-Barbara, United States. ⟨hal-01588422⟩

Florent Saudel, Sandrine Blazy, Frédéric Besson. Confusion de Type en C++: État de l'Art et Difficultés de Détection. 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. ⟨hal-01656979⟩

Frédéric Besson, Sandrine Blazy, Pierre Wilke. CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics. ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. pp.81-97, ⟨10.1007/978-3-319-66107-0_6⟩. ⟨hal-01656875⟩

Sandrine Blazy, David Pichardie, Alix Trieu. Verifying Constant-Time Implementations by Abstract Interpretation. European Symposium on Research in Computer Security, Sep 2017, Oslo, Norway. ⟨hal-01588444⟩

Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, et al.. Closing the Gap – The Formally Verified Optimizing Compiler CompCert. SSS'17: Safety-critical Systems Symposium 2017, Feb 2017, Bristol, United Kingdom. pp.163-180. ⟨hal-01399482⟩

Sandrine Blazy, Alix Trieu. Formal Verification of Control-flow Graph Flattening. Certified Proofs and Programs (CPP 2016), Jan 2016, Saint-Petersburg, United States. pp.12, ⟨10.1145/2854065.2854082⟩. ⟨hal-01242063⟩

Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, et al.. CompCert - A Formally Verified Optimizing Compiler. ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, Jan 2016, Toulouse, France. ⟨hal-01238879⟩

Sandrine Blazy, Vincent Laporte, David Pichardie. An Abstract Memory Functor for Verified C Static Analyzers. ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. pp.14, ⟨10.1145/2951913.2951937⟩. ⟨hal-01339969⟩

Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent. Data Tainting and Obfuscation: Improving Plausibility of Incorrect Taint. Source Code Analysis and Manipulation (SCAM), Sep 2015, Bremen, Germany. ⟨hal-01193286⟩

Sandrine Blazy. Formal verification of compilers and static analyzers. . PLMW@POPL 2015 - Programming Languages Mentoring Workshop, Jan 2015, Mumbai, India. ⟨hal-01242094⟩

Sandrine Blazy, Delphine Demange, David Pichardie. Validating Dominator Trees for a Fast, Verified Dominance Test. Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_6⟩. ⟨hal-01193281⟩

Sandrine Blazy, Andre Maroneze, David Pichardie. Verified Validation of Program Slicing. CPP 2015 : Conference on Certified Programs and Proofs, 2015, Mumbai, India. pp.109-117, ⟨10.1145/2676724.2693169⟩. ⟨hal-01110821⟩

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie. A formally-verified C static analyzer. POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩. ⟨hal-01078386⟩

Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Concrete Memory Model for CompCert. ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. pp.67-83, ⟨10.1007/978-3-319-22102-1_5⟩. ⟨hal-01194549⟩

Sandrine Blazy, Stéphanie Riaud. Measuring the Robustness of Source Program Obfuscation - Studying the Impact of Compiler Optimizations on the Obfuscation of C Programs. Fourth ACM Conference on Data and Application Security and Privacy - SIGSAC ACM CODASPY 2014, Mar 2014, San Antonio, United States. ⟨hal-00927427⟩

Sandrine Blazy, David Bühler, Boris Yakobowski. Improving static analyses of C programs with conditional predicates. FMICS 2014: Formal Methods for Industrial Critical Systems, Sep 2014, Florence, Italy. pp.15, ⟨10.1007/978-3-319-10702-8_10⟩. ⟨hal-01242087⟩

Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. The 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. pp.128 - 143, ⟨10.1007/978-3-319-08970-6_9⟩. ⟨hal-01102445⟩

André Oliveira Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut. A Formally Verified WCET Estimation Tool. 14th International Workshop on Worst-Case Execution Time Analysis, Jul 2014, Madrid, Spain. ⟨10.4230/OASIcs.WCET.2014.11⟩. ⟨hal-01087194⟩

Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Precise and Abstract Memory Model for C Using Symbolic Values. 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. pp.449 - 468, ⟨10.1007/978-3-319-12736-1_24⟩. ⟨hal-01093312⟩

Jael Kriener, Andy King, Sandrine Blazy. Proofs You Can Believe In. Proving Equivalences Between Prolog Semantics in Coq. 15th International Symposium on Principles and Practice of Declarative Programming (PPDP), Sep 2013, Madrid, Spain. pp.37-48. ⟨hal-00908848⟩

Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344. ⟨hal-00812515⟩

Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. VSTTE - Verified Software: Theories, Tools and Experiments, Natarajan Shankar, May 2013, Menlo Park, United States. pp.281-303. ⟨hal-00848703⟩

Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, et al.. Formally verified optimizing compilation in ACG-based flight control software. ERTS2 2012: Embedded Real Time Software and Systems, AAAF, SEE, Feb 2012, Toulouse, France. ⟨hal-00653367⟩

Sandrine Blazy, Roberto Giacobazzi. Towards a formally verified obfuscating compiler. SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, ACM SIGPLAN, Jun 2012, Beijing, China. ⟨hal-00762330⟩

Sandrine Blazy, Benoît Robillard, Andrew W. Appel. Formal Verification of Coalescing Graph-Coloring Register Allocation. 19th European Symposium on Programming (ESOP), Mar 2010, Paphos, Cyprus. pp.145-164. ⟨inria-00477689⟩

Sandrine Blazy, Benoit Robillard. Live-Range Unsplitting for Faster Optimal Coalescing. LCTES'09 ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems, Jan 2009, X, France. pp.70-79. ⟨hal-01125616⟩

Sandrine Blazy, Benoît Robillard. Register allocation by graph coloring under full live-range splitting. ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded systems (LCTES'2009), ACM, Jun 2009, Dublin, Ireland. ⟨inria-00387749⟩

Sandrine Blazy, Benoit Robillard, Eric Soutif. Coloration avec préférences : complexité, inégalités valides et vérification formelle. ROADEF'08, Clermont-Ferrand, 25-27 Février, Jan 2008, X, France. pp.123-138. ⟨hal-01125409⟩

Sandrine Blazy, Benoît Robillard, Eric Soutif. Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe. JFLA (Journées Francophones des Langages Applicatifs), INRIA, Jan 2008, Etretat, France. pp.31-46. ⟨inria-00202713⟩

Sandrine Blazy. Which C semantics to embed in the front-end of a formally verified compiler?. TTVSI (Tools and Techniques for Verification of System Infrastructure), Mar 2008, Oxford, United Kingdom. pp.31. ⟨inria-00292441⟩

Benoît Robillard, Sandrine Blazy, Eric Soutif. Coloration avec préférences : complexité, inégalités valides et vérification formelle. 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. ⟨inria-00260712⟩

Sandrine Blazy, Benoit Robillard, Eric Soutif. Coloration avec préférences dans les graphes triangulés. Journées Graphes et Algorithmes, Paris, Jan 2007, X, France. pp.32. ⟨hal-01125410⟩

Sandrine Blazy, Benoît Robillard, Eric Soutif. Coloration avec préférences dans les graphes triangulés. Journées Graphes et algorithmes (JGA'07), Nov 2007, Paris, France. pp.32. ⟨inria-00292045⟩

Andrew W. Appel, Sandrine Blazy. Separation Logic for Small-step Cminor. 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. pp.5-21. ⟨inria-00165915⟩

Sandrine Blazy. Experiments in validating formal semantics for C. C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp.95-102. ⟨inria-00292043⟩

Sandrine Blazy, Zaynah Dargaye, Xavier Leroy. Formal Verification of a C Compiler Front-end. FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. pp.460-475, ⟨10.1007/11813040_31⟩. ⟨inria-00106401⟩

Sandrine Blazy, Xavier Leroy. Formal verification of a memory model for C-like imperative languages. ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. pp.280-299, ⟨10.1007/11576280⟩. ⟨inria-00077921⟩

Sandrine Blazy, Frédéric Gervais, Régine Laleau. Une démarche outillée pour spécifier formellement des patrons de conception réutilisables. Objets, Composants et Modèles dans l'ingénierie des SI, Jan 2003, X, France. ⟨hal-01124805⟩

Sandrine Blazy, Frédéric Gervais, Régine Laleau. Reuse of Specification Patterns with the B Method. ZB 2003: Formal Specification and Development in Z and B, Jun 2003, Turku, Finland, pp.40-57. ⟨inria-00078953⟩

St?phanie Bocs, Sandrine Blazy, Claudine M?digue, Paul Glaser. An automatic detection of prokaryotic CoDing Sequences Combining Several Independent Methods. Genome 2000, Paris, Jan 2000, X, France. ⟨hal-01124664⟩

Sandrine Blazy, Philippe Facon. Partial Evaluation for Program Comprehension. ACM Computing Surveys, Symposium on partial evaluation, 1998, (revue électonique). ⟨inria-00106403⟩

Sandrine Blazy, Philippe Facon. Application of formal methods to the development of a software maintenance tool. ASE'97: The 12th IEEE Conference on Automated Software Engineering., Lowry, M. and Ledru, Y., Nov 1997, Lake Tahoe, Nevada, USA, pp.162-171. ⟨inria-00078882⟩

Sandrine Blazy, Philippe Facon. An automatic interprocedural analysis for the understanding of scientific application programs. Dagstuhl seminar on partial evaluation, Feb 1996, Saarbrucken, Germany. pp.1-16, ⟨10.1007/3-540-61580-6⟩. ⟨inria-00165927⟩

Sandrine Blazy, Philippe Facon. Interprocedural analysis for program comprehension by specialization. 4th IEEE Workshop on Program Comprehension, Berlin, Jan 1996, X, France. pp.133-141. ⟨hal-01124465⟩

Sandrine Blazy, Philippe Facon. Formal specification and prorotyping of a program specializer. TAPSOFT'95, Aarhus, Jan 1995, X, France. pp.666-680. ⟨hal-01124466⟩

Sandrine Blazy, Philippe Facon. Formal specification and prototyping of a program specializer. 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⟩. ⟨inria-00165933⟩

Sandrine Blazy, Philippe Facon. SFAC, a tool for program comprehension by specialization. IEEE Third Workshop on Program Comprehension, Nov 1994, Washington D.C., United States. pp.162-167, ⟨10.1109/WPC.1994.341266⟩. ⟨inria-00165938⟩

Sandrine Blazy, Philippe Facon. Partial evaluation as an aid to the comprehension of Fortran programs. 2nd IEEE Workshop on Program Comprehension, Capri, Italy, Jan 1993, X, France. pp.46-54. ⟨hal-01124468⟩

Sandrine Blazy, Philippe Facon. Partial evaluation and symbolic computation for the understanding of Fortran programs. Advanced Information Systems Engineering 5th International Conference, CAiSE '93, 1993, Paris, France. pp.184-198, ⟨10.1007/3-540-56777-1⟩. ⟨inria-00165950⟩

Sandrine Blazy, Philippe Facon. Evaluation partielle pour la compréhension de programmes Fortran. Software Engineering and its applications, Toulouse, December, Dec 1992, X, France. pp.411-417. ⟨hal-01124469⟩

Marc Haziza, Jean-François Voidrot, Jean-Pierre Queille, Lech Pofelski, Sandrine Blazy. Software maintenance: an analysis of industrial needs and constraints. IEEE Conference on Software Maintenance, IEEE, Nov 1992, Orlando, USA, France. pp.18-26, ⟨10.1109/ICSM.1992.242563⟩. ⟨inria-00143556⟩

Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart. The CompCert memory model. Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010. ⟨hal-00905435⟩

Sandrine Blazy, Marsha Chechik. Verified Software: Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Toronto, Canada, July 17-18, 2016. Proceedings. Sandrine Blazy and Marsha Chechik. Verified Software: Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Jul 2016, Toronto, Canada. 9971, Springer, 2016, Lecture Notes in Computer Science. ⟨hal-01387207⟩

Sandrine Blazy, Thomas Jensen. Static Analysis Symposium - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015. Proceedings. Sandrine Blazy; Thomas Jensen. Static Analysis Symposium - 22nd International Symposium, SAS 2015, Aug 2015, Saint-Malo, France. Lecture Notes in Computer Science (LNCS) (9291), Springer, pp.335, 2015, 978-3-662-48287-2. ⟨hal-01194558⟩

Sandrine Blazy, Christine Paulin-Mohring, David Pichardie. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David. Rennes, France. 7998, Springer, pp.500, 2013, Lecture Notes in Computer Science, ⟨10.1007/978-3-642-39634-2⟩. ⟨hal-00908865⟩

Sandrine Blazy. Actes de la conférence JFLA2008 (Journées Francophones des Langages Applicatifs). INRIA. INRIA, pp.173, 2008, 2-7261-1295-1. ⟨inria-00202715⟩

Sandrine Blazy. Actes de la conférence JFLA2008. INRIA. 2008. ⟨hal-01125405⟩

Sandrine Blazy. Sémantiques formelles. Informatique [cs]. Université d'Evry-Val d'Essonne, 2008. ⟨tel-00336576⟩