Page de Sandrine Blazy

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Formal verification of a C compiler front-end

LNCS 4085

LNCS 3785

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.

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.

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.

ACM Computing Surveys

Vol.30, N°3es

IEEE Conf. on Automated Software Engineering

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.

LNCS 915

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.

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).

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.

Sandrine Blazy

Publications

2018

2017

2016

2015

2014

2013

2012

2010

2009

2008

2007

2006

2005

2003

2002

2000

1998

1997

1996

1995

1994

1993

1992