Sandrine Blazy

• Home
• Publications
• Students
• Thesis Committees

Publications

See also HAL, Google Scholar and ORCID

2025

• Tony Law, Delphine Demange, Sandrine Blazy. A Mechanized Semantics for Dataflow Circuits. ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (OOPSLA 2025). To appear.
• Roméo La Spina, Delphine Demange, Sandrine Blazy. Formal Verification of WTO-based Dataflow Solvers. 25th European Symposium On Programming (ESOP 2025). To appear.

2024

• Sandrine Blazy. From mechanized semantics to verified compilation: the Clight semantics of CompCert. FASE 2024 (Fundamental Approaches to Software Engineering), Luxembourg, 8-12/04/2024. Lecture Notes in Computer Science (LNCS) n°14573, pp. 1-21.

2023

• Yann Herklotz, Delphine Demange, Sandrine Blazy. Mechanised Semantics for Gated Static Single Assignment. 12th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2023, pp. 182-196.
• 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. 50th ACM SIGPLAN Symposium on Principles on Programming Languages, POPL 2023, vol. 7, article n°9, pp.249-277.

2021

• Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie. Secure Compilation of Constant-resource Programs. CSF 2021, 34th IEEE Computer Security Foundations Symposium, 22-24 June 2021, pp.207-218.
• Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek. Formally Verified Speculation and Deoptimization in a JIT Compiler. 48th ACM SIGPLAN Symposium on Principles on Programming Languages, POPL 2021, vol.5, pp. 1-26.

2020

• Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie. A Fast Verified Liveness Analysis in SSA Form. IJCAR 2020 (International Joint Conference on Automated Reasoning), Paris, 01-04/07/2020. Lecture Notes in Computer Science (LNCS) n°12167, pp. 324-340.
• Aurèle Barrière, Sandrine Blazy, David Pichardie. Towards Formally Verified Just-in-Time compilation. 6th workshop on Coq for Programming Languages, CoqPL 2020.
• Sandrine Blazy, Rémi Hutin, David Pichardie. A CompCert Compiler that Preserves Cryptographic Constant-time. 3rd Principles of Secure Compilation workshop, PriSC 2020.
• 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. 47th ACM SIGPLAN Symposium on Principles on Programming Languages, POPL 2020, vol.4, pp. 7:1-7:30.

2019

• Sandrine Blazy. Teaching Deductive Verification in Why3 to Undergraduate Students. FMTea 2019 (Formal Methods Teaching Workshop and Tutorial), Porto, Protugal, 7/10/2019. Lecture Notes in Computer Science (LNCS) n°11758, pp. 1-15.
• Frédéric Besson, Sandrine Blazy, Pierre Wilke. CompCertS: a Memory-aware Verified Compiler using a Pointer as Integer Semantics. Journal of Automated Reasoning, 63(2), 08/2019, Springer, pp.369-392.
• 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, 62(4), 04/2019, Springer, pp.433-480.
• Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas Jensen, Pierre Wilke. Compiling Sandboxes: Formally Verified Software Fault Isolation. 19th European Symposium On Programming (ESOP 2019), Prague, Czech Republic, 8-11/04/2019. Lecture Notes in Computer Science (LNCS) n°11423, pp. 499-524.
• Sandrine Blazy, David Pichardie, Alix Trieu. Verified Constant-Time Implementations by Abstract Interpretation (extended version). Journal of Computer Security, 27(1), January 2019, pp. 137-163.
• Sandrine Blazy, Rémi Hutin. Formal verification of a program obfuscation based on mixed boolean-arithmetic expressions. CPP 2019 - Certified Proofs and Programs, Lisbon, Portugal, 14-15/01/2019, ACM, pp.196-208.

2018

• Sandrine Blazy, Marsha Chechik. Selected Extended Papers of VSTTE 2016. Journal of Automated Reasoning, 60(3), 03/2018.
• Daniel Kästner, Ulrich Wünsche, Jörg Barrho, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. Embedded Real Time Software and Systems (ERTS 2018). SEE, 01/2018.

2017

• Sandrine Blazy, Pierre Castéran, Hugo Herbelin. L'assitant de preuve Coq. Techniques de l'ingénieur, August 2017.
• Frédéric Besson, Sandrine Blazy, Pierre Wilke. CompCertS: a memory-aware verified C compiler using pointer as integer semantics. ITP 2017, 8th Interactive Theorem Proving conference, Brasilia, Brazil, 26-29 September 2017. Lecture Notes in Computer Science (LNCS) n°10499, Springer, pp.81-97.
• Sandrine Blazy, David Pichardie, Alix Trieu. Verified Constant-Time Implementations by Abstract Interpretation. ESORICS 2017, 22nd European Symposium on Research in Computer Security, Oslo, 11-13 September 2017. Lecture Notes in Computer Science (LNCS) n°10492, Springer, pp. 260-277.
• Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu. Verified Translation Validation of Static Analyses. CSF 2017, 30th IEEE Computer Security Foundations Symposium, Santa Barbara, 21-25 August 2017. pp. 405-419.
• Sandrine Blazy, David Bühler, Boris Yakobowski. Structuring Abstract Interpreters through State and Value Abstractions. VMCAI 2017, 18th International Conference on Verification, Model Checking and Abstract Interpretation, Paris, 22-24 January 2017. Lecture Notes in Computer Science (LNCS) n°10145, Springer, pp. 112-130.
• Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, Christian Ferdinand. Closing the gap - The formally verified compiler CompCert. 25th Safety-critical Systems Symposium 2017 (SSS 2017), Bristol, United Kingdom, 07/02/2017. CreateSpace, pp.163-180.

2016

• Sandrine Blazy, Marsha Chechik. Proceedings of Verified Software: Theories, Tools, and Experiments-8th International Conference (VSTTE 2016), Toronto, Canada, 17-18 July , 2016. Lecture Notes in Computer Science 9971, Springer.
• Sandrine Blazy, Vincent Laporte, David Pichardie. An Abstract Memory Functor for Verified C Static Analyzers. ICFP'16 - 21st ACM SIGPLAN International Conference on Functional Programming, Nara, Japan, pp. 325-337, 09/2016.
• Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-Modifying Code. Extended version, Journal of Automated Reasoning, 56(3), pp. 283-308, 03/2016.
• Sandrine Blazy, David Bühler, Boris Yakobowski. Improving Static Analyses of C Programs with Conditional Predicates. Science of Computer Programming, volume 118, 03/2016, pp. 77-95, Elsevier.
• Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, Christian Ferdinand. CompCert - A formally verified optimizing compiler Embedded Real Time Software and Systems (ERTS2 2016), Toulouse, France, 27-29/01/2016. pp 188-195.
  President's favorite award.
  
• Sandrine Blazy, Alix Trieu. Formal verification of control-flow flattening. CPP 2016 - Certified Proofs and Programs, Saint Petersburg, USA, 18-19/01/2016, ACM, pp.176-187.

2015

• Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent. Data tainting and Obfuscation: Improving Plausibility of Incorrect Taint. 15th conference on Source Code Analysis and Manipulation, SCAM 2015, Bremen, Germany, September 2015, IEEE, pp. 111-120.
• Sandrine Blazy, Thomas Jensen. Proceedings of the 22nd International Static Analysis Symposium (SAS 2015), Saint-Malo, France, 9-11 september, 2015. Lecture Notes in Computer Science 9291, Springer.
• Sandrine Blazy, Delphine Demange, David Pichardie. Validating Dominator Trees for a Fast, Verified Dominance Test. ITP-6th Interactive Theorem Proving conference, Nanjing, China, August 2015. Lecture Notes in Computer Science (LNCS) n°9236, Springer, pp.84-99.
• Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Concrete Memory Model for CompCert. ITP-6th Interactive Theorem Proving conference, Nanjing, China, August 2015. Lecture Notes in Computer Science (LNCS) n°9236, Springer, pp.67-83.
• Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie. A formally C static analyzer. 42nd Symposium on Principles on Programming Languages, POPL 2015, Mumbai, India, January 2015, ACM, pp. 247-259.
• Sandrine Blazy. Formal verification of compilers and static analyzers. Programming Languages Mentoring Workshop, PLMW@POPL 2015, Mumbai, India, 14/01/2015, pp.9, ACM.
• Sandrine Blazy, André Oliveria Maroneze, David Pichardie. Verified validation of program slicing. CPP 2015 - Certified Proofs and Programs, Mumbai, India, January 2015, ACM, pp.109-117.

2014

• 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. Lecture Notes in Computer Science (LNCS) n°8858, Springer, pp.449-468.
• Sandrine Blazy, David Bühler, Boris Yakobowski. Improving Static Analyses of C Programs with Conditional Predicates. Formal Methods for Industrial Critical Systems, FMICS 2014, 19th international workshop on Formal Methods for Industrial Critical Systems. Lecture Notes in Computer Science (LNCS) n°8718, Springer, pp.140-154.
  Best paper award.
  
• André Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut. A Formally Verified WCET Estimation Tool. 14th International workshop on worst-case execution time analysis, WCET 2014, Madrid, Spain, July 2014, pp. 11-20.
• Xavier Leroy, Andrew Appel, Sandrine Blazy, Gordon Stewart. The CompCert memory model. Cambridge University Press. 2014. In Program Logics for Certified Compilers.
• Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-Modifying Code. ITP-5th Interactive Theorem Proving conference, Vienna, Austria, July 2014. Lecture Notes in Computer Science (LNCS) n°8558, Springer, pp.128-143.
• Sandrine Blazy, Stéphanie Riaud. Measuring the robustness of source program obfuscation. CODASPY 2014 - 4th ACM Conference on Data and Application Security and Privacy, San Antonio, USA, March 2014, pp.123-126.

2013

• Jael Kriener, Andy King, Sandrine Blazy. Proofs you can believe in - Proving equivalences between Prolog semantics in Coq. PPDP'13 - 15th International Symposium on Principles and Practice of Declarative Programming, Madrid, Spain, September 2013. ACM, pp.37-48.
• Sandrine Blazy, Christine Paulin-Mohring, David Pichardie. Interactive Theorem Proving conference (ITP 2013), Rennes, France, July 2013. Lecture Notes in Computer Science (LNCS) n°7998, Springer.
• Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal verification of a C Value Analysis Based on Abstract Interpretation. SAS - 20th Static Analysis Symposium, Seattle, USA, June 2013. Lecture Notes in Computer Science (LNCS) n°7935, Springer, pp.324-344.
• Sandrine Blazy, André Maroneze, David Pichardie. Formal verification of Loop Bound Estimation for WCET Analysis. VSTTE - Verified Software: Theories, Tools and Experiments, Atherton, USA, May 2013. Lecture Notes in Computer Science (LNCS) n°8164, Springer, pp.281-303.

2012

• Ricardo Bedin França, Sandrine Blazy, Denis Favre-Félix, Xavier Leroy, Marc Pantel, Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. ERTS2 2012: Embedded Real Time Software and Systems, Toulouse, March 2012.
• Sandrine Blazy, Roberto Giaccobazzi. Towards an obfuscating compiler. SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, Beijing, China, July 2012.

2010

• Sandrine Blazy, Benoît Robillard, Andrew W.Appel. Formal Verification of Coalescing Graph-Coloring Register Allocation. 19th Euopean Symposium On Programming (ESOP 2010), Paphos, Cyprus, March 2010. Lecture Notes in Computer Science (LNCS) n°6012, Springer, pp.145-164.

2009

• Sandrine Blazy, Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning. 43(3), pp. 263-288, October 2009.
• 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), pp.70-79, Dublin, 19-20 juin 2009.

2008

• Sandrine Blazy. Sémantiques formelles. Habilitation à diriger des recherches. Université d'Évry Val d'Essonne. 23 octobre 2008.
• Xavier Leroy, Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning. 41(1), pp.1-31, July 2008.
• 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), en l'honneur des 60 ans du professeur Michael J.C.Gordon, Londres, 25-26 mars 2008.
• Benoît Robillard, Sandrine Blazy, Éric 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, Clermont-Ferrand, 25-27 février 2008, pp.123-138.
• Sandrine Blazy, Benoît Robillard, Éric Soutif. Vérification formelle d'un algorithme d'allocation de registres par coloration de graphes. Journées Françaises des Langages Applicatifs (JFLA'08), Étretat, 26-29 janvier 2008, pp.31-46.

2007

• Sandrine Blazy. Comment gagner confiance en C ?. TSI, numéro spécial "Langages applicatifs", Volume 26, numéro 9, 2007, pp.1195-1200.
• Sandrine Blazy, Benoît Robillard, Éric Soutif. Coloration avec préférences dans les graphes triangulés.Journées Graphes et algorithmes (JGA'07), Paris, 8-9 novembre 2007, p.32.
• Andrew W. Appel, Sandrine Blazy. Separation logic for small-step Cminor. 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Kaiserslautern, Germany 10-13 September 2007. LNCS 4732, pp.5-21.
• Sandrine Blazy. Experiments in validating formal semantics for C. C/C++ Verification Workshop, Oxford, United Kingdom, 2 July 2007. Raboud University Nijmegen report ICIS-R07015, pp.95-102.
• Andrew W.Appel, Sandrine Blazy.Separation logic for small-step Cminor (extended version). INRIA research report RR-6138, March 2007, 29 pages.

2006

Sandrine Blazy, Zaynah Dargaye, Xavier Leroy. Formal verification of a C compiler front-end. FM'06, 14th Symposium on Formal Methods, Hamilton, Canada, 23-25 August 2006. LNCS 4085, pp.460-475.

2005

Sandrine Blazy, Xavier Leroy.Formal verification of a memory model for C-like imperative languages. ICFEM'05: 7th Int. Conference on Formal Engineering Methods, Manchester, UK, 1-4 November 2005. LNCS 3785, pp.280-299.

2003

• Sandrine Blazy, Frédéric Gervais, Régine Laleau. Une démarche outillée pour spécifier formellement des patrons de conception réutilisables. Workshop Objets, Composants et Modèles dans l'ingénierie des SI, associé à INFORSID'2003, Nancy, 3 juin 2003.
• Sandrine Blazy, Frédéric Gervais, Régine Laleau. Reuse of specification patterns with the B method. ZB 2003 3rd Int. Conference of B and Z Users, Turku, Finland, 4-6 June 2003, LNCS 2651, pp.40-57.

2002

• Sandrine Blazy, Frédéric Gervais, Régine Laleau. Un exemple de réutilisation de patterns de spécification avec la méthode B. Rapport technique CEDRIC N°395.
• Sandrine Blazy. Transformations certifiées de programmes impératifs. Rapport technique CEDRIC N°398.

2000

• Sandrine Blazy. Specifying and Automatically Generating a Specialization Tool for Fortran 90. Journal on Automated Software Engineering, Vol.7, N°4, December 2000, pp.345-376.
• Stéphanie Bocs, Sandrine Blazy, P.Glaser, Claudine Médigue. An automatic detection of prokaryotic CoDing Sequences Combining Several Independant Methods. Genome 2000, Int. Conf. on Microbial and Model Genomes, Paris, 11-15 April 2000.

1998

• Sandrine Blazy, Philippe Facon. Partial evaluation for program comprehension. ACM Computing Surveys, Symposium on partial evaluation, Vol.30, N°3es, September 1998.

1997

• Sandrine Blazy, Philippe Facon. Application of formal methods to the development of a software maintenance tool. IEEE Conf. on Automated Software Engineering, Lake Tahoe, 3-5 November 1997, pp.162-171.

1996

• Sandrine Blazy, Philippe Facon. Interprocedural analysis for program comprehension by specialization. 4th IEEE Workshop on Program Comprehension, Berlin, 29-31 March 1996, pp.133-141.
• Sandrine Blazy, Philippe Facon. An automatic interprocedural analysis for the understanding of scientific application programs. Seminar on partial evaluation, Dagsthul castle 12-16 February 1996, LNCS 1110, pp.1-16.

1995

• Sandrine Blazy, Philippe Facon. Formal specification and prorotyping of a program specializer. TAPSOFT'95, Aarhus, 22-26 May 1995, LNCS 915, pp.666-680.

1994

• Sandrine Blazy, Philippe Facon. SFAC: a tool for program comprehension by specialization. 3rd IEEE Workshop on Program Comprehension, Washington D.C., 14-15 November 1994, pp.162-167.
• Sandrine Blazy, Philippe Facon. Partial evaluation for the understanding of Fortran programs. Int. Journal of Software Engineering and Knowledge Engineering (IJSEKE), 4(4), December 1994, pp.535-559.

1993

• Sandrine Blazy, Philippe Facon Partial evaluation as an aid to the comprehension of Fortran programs. 2nd IEEE Workshop on Program Comprehension, Capri, Italy, July 1993, pp.46-54.
• Sandrine Blazy, Philippe Facon Partial evaluation for the understanding of Fortran programs. Software Engineering and Knowledge Engineering (SEKE), San Francisco, June 1993, pp.517-525. Awarded best student paper.
• Sandrine Blazy, Philippe Facon Partial evaluation and symbolic computation for the understanding of Fortran programs. CAISE'93, Paris, June 1993, LNCS 685, pp.184-198.
• Sandrine Blazy La spécialisation de programmes pour l'aide à la maintenance du logiciel. CNAM, 1993, PhD thesis (in French).

1992

• Marc Haziza, Jean-François Voidrot, Earl Minor, Lech Pofelski, Sandrine Blazy. Software maintenance: an analysis of industrial needs and constraints. IEEE Confrence Software Maintenance, Orlando, USA, 9-12 November 1992, pp.18-26.
• Sandrine Blazy, Philippe Facon. Évaluation partielle pour la compréhension de programmes Fortran. Software Engineering and its applications, Toulouse, December 1992, pp.411-417.

Page designed by Mike Cronin via OSWD