2019

  • 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. XX-XX.
  • 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

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

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

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

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

1997

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.