Mots-clés

Identifiants chercheur

Nombre de documents

70

Sandrine Blazy


Article dans une revue10 documents

  • 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〉
  • 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, 2017, pp.1-48. 〈10.1007/s10817-017-9439-z〉. 〈hal-01656895〉
  • 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〉

Communication dans un congrès53 documents

  • 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 - Embedded Real Time Software and Systems, Jan 2018, Toulouse, France. 2018, 〈https://www.erts2018.org/〉. 〈hal-01643290〉
  • 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. CreateSpace, pp.163-180, 2017, Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium. 〈hal-01399482〉
  • Sandrine Blazy, David Pichardie, Alix Trieu. Verifying Constant-Time Implementations by Abstract Interpretation. European Symposium on Research in Computer Security, Sep 2017, Oslo, Norway. 22nd European Symposium on Research in Computer Security. 〈hal-01588444〉
  • 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. Springer, LNCS, 10499, pp.81-97, ITP 2017: Interactive Theorem Proving. 〈http://itp2017.cic.unb.br/〉. 〈10.1007/978-3-319-66107-0_6〉. 〈hal-01656875〉
  • 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. 30th IEEE Computer Security Foundations Symposium. 〈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, 2017, 〈https://ressi2017.sciencesconf.org/〉. 〈hal-01656979〉
  • 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, Jan 2016, Toulouse, France. 〈http://www.erts2016.org/〉. 〈hal-01238879〉
  • Sandrine Blazy, Alix Trieu. Formal Verification of Control-flow Graph Flattening. ACM. Certified Proofs and Programs (CPP 2016), Jan 2016, Saint-Petersburg, United States. pp.12, 2016, Certified Proofs and Programs (CPP 2016). 〈https://people.csail.mit.edu/adamc/cpp16/index.html〉. 〈10.1145/2854065.2854082〉. 〈hal-01242063〉
  • 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. ACM, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), pp.14, 2016, 〈http://conf.researchr.org/home/icfp-2016/〉. 〈10.1145/2951913.2951937〉. 〈hal-01339969〉
  • 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. ACM, pp.247-259, 〈10.1145/2676726.2676966〉. 〈hal-01078386〉
  • Sandrine Blazy, Delphine Demange, David Pichardie. Validating Dominator Trees for a Fast, Verified Dominance Test. Springer. Interactive Theorem Proving, Aug 2015, Nanjing, China. Lecture Notes in Computer Science (LNCS) (9236), 2015, 〈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〉
  • Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Concrete Memory Model for CompCert. Springer. ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. Lecture Notes in Computer Science (LNCS) (9236), pp.67-83, 2015, nteractive Theorem Proving. 〈10.1007/978-3-319-22102-1_5〉. 〈hal-01194549〉
  • Sandrine Blazy. Formal verification of compilers and static analyzers. . PLMW@POPL 2015 - Programming Languages Mentoring Workshop, Jan 2015, Mumbai, India. 〈hal-01242094〉
  • Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent. Data Tainting and Obfuscation: Improving Plausibility of Incorrect Taint. IEEE. Source Code Analysis and Manipulation (SCAM), Sep 2015, Bremen, Germany. 〈hal-01193286〉
  • 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. Springer, 8558, pp.128 - 143, 2014, LNCS : Interactive Theorem Proving. 〈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. 2014, 〈http://www.uni-ulm.de/en/in/wcet2014.html〉. 〈10.4230/OASIcs.WCET.2014.11〉. 〈hal-01087194〉
  • 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. Lecture Notes in Computer Science (LNCS) (8718), pp.15, 2014, FMICS 2014: Formal Methods for Industrial Critical Systems. 〈http://fmics2014.unifi.it〉. 〈10.1007/978-3-319-10702-8_10〉. 〈hal-01242087〉
  • 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. Springer, 8858, pp.449 - 468, 2014, LNCS. 〈10.1007/978-3-319-12736-1_24〉. 〈hal-01093312〉
  • 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. 2014. 〈hal-00927427〉
  • Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. Manuel Fahndrich and Francesco Logozzo. SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. Springer, Lecture Notes in Computer Science, pp.324-344, 2013, 7935. 〈hal-00812515〉
  • Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. Ernie Cohen and Andrey Rybalchenko. VSTTE - Verified Software: Theories, Tools and Experiments, May 2013, Menlo Park, United States. Springer, 8164, pp.281-303, 2013, Lecture Notes in Computer Science. 〈hal-00848703〉
  • Jael Kriener, Andy King, Sandrine Blazy. Proofs You Can Believe In. Proving Equivalences Between Prolog Semantics in Coq. Tom Schrijvers. 15th International Symposium on Principles and Practice of Declarative Programming (PPDP), Sep 2013, Madrid, Spain. ACM, pp.37-48, 2013. 〈hal-00908848〉
  • Sandrine Blazy, Roberto Giacobazzi. Towards a formally verified obfuscating compiler. Christian Collberg. SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, Jun 2012, Beijing, China. ACM SIGPLAN, 2012. 〈hal-00762330〉
  • 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, Feb 2012, Toulouse, France. 2012. 〈hal-00653367〉
  • Sandrine Blazy, Benoît Robillard, Andrew W. Appel. Formal Verification of Coalescing Graph-Coloring Register Allocation. Andrew Gordon. 19th European Symposium on Programming (ESOP), Mar 2010, Paphos, Cyprus. Springer, 6012, pp.145-164, 2010, Lecture Notes in Computer Science. 〈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, 2009, ACM. 〈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), Jun 2009, Dublin, Ireland. 2009. 〈inria-00387749〉
  • Sandrine Blazy, Benoit Robillard, Eric Soutif. Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe. JFLA'08 Journ?es Francophones des Langages Applicatifs, Jan 2008, X, France. pp.31-46, 2008. 〈hal-01125406〉
  • 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, 2008. 〈hal-01125409〉
  • 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, 2008. 〈inria-00292441〉
  • 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), Jan 2008, Etretat, France. pp.31-46, 2008. 〈inria-00202713〉
  • Benoît Robillard, Sandrine Blazy, Eric Soutif. Coloration avec préférences : complexité, inégalités valides et vérification formelle. Presses Universitaires de l'Université Blaise Pascal. ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, Feb 2008, Clermont-Ferrand, France. pp.123-138, 2008. 〈inria-00260712〉
  • Andrew W. Appel, Sandrine Blazy. Separation Logic for Small-step Cminor. Springer-Verlag. 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. 4732, pp.5-21, 2007, Lecture Notes in Computer Science. 〈inria-00165915〉
  • 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, 2007. 〈hal-01125410〉
  • Sandrine Blazy. Experiments in validating formal semantics for C. C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp.95-102, 2007. 〈inria-00292043〉
  • 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, 2007. 〈inria-00292045〉
  • Sandrine Blazy, Zaynah Dargaye, Xavier Leroy. Formal Verification of a C Compiler Front-end. Jayadev Misra, Tobias Nipkow and Emil Sekerinski. FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. Springer-Verlag, 4085 (4085), pp.460-475, 2006, Lecture Notes in Computer Science. 〈10.1007/11813040_31〉. 〈inria-00106401〉
  • Sandrine Blazy, Xavier Leroy. Formal verification of a memory model for C-like imperative languages. Kung-Kiu Lau, Richard Banach. ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. Springer, 3785 (3785), pp.280-299, 2005, Lecture Notes in Computer Science. 〈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. 2003. 〈hal-01124805〉
  • Sandrine Blazy, Frédéric Gervais, Régine Laleau. Reuse of Specification Patterns with the B Method. Springer-Verlag. ZB 2003: Formal Specification and Development in Z and B, Jun 2003, Turku, Finland, 2651 (2651), pp.40-57, 2003, Lecture Notes in Computer Science. 〈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. 2000. 〈hal-01124664〉
  • Sandrine Blazy, Philippe Facon. Partial Evaluation for Program Comprehension. ACM. ACM Computing Surveys, Symposium on partial evaluation, 1998, (revue électonique), 30/3 es (3 es), 1998. 〈inria-00106403〉
  • Sandrine Blazy, Philippe Facon. Application of formal methods to the development of a software maintenance tool. IEEE CS Press. ASE'97: The 12th IEEE Conference on Automated Software Engineering., Nov 1997, Lake Tahoe, Nevada, USA, pp.162-171, 1997. 〈inria-00078882〉
  • Sandrine Blazy, Philippe Facon. An automatic interprocedural analysis for the understanding of scientific application programs. Springer Verlag. Dagstuhl seminar on partial evaluation, Feb 1996, Saarbrucken, Germany. 1110, pp.1-16, Lecture Notes in Computer Science. 〈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, 1996. 〈hal-01124465〉
  • Sandrine Blazy, Philippe Facon. Formal specification and prototyping of a program specializer. Springer Verlag. TAPSOFT '95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE, May 1995, Aarhus, Denmark. 915, pp.666-680, Lecture Notes in Computer Science. 〈10.1007/3-540-59293-8_227〉. 〈inria-00165933〉
  • Sandrine Blazy, Philippe Facon. Formal specification and prorotyping of a program specializer. TAPSOFT'95, Aarhus, Jan 1995, X, France. pp.666-680, 1995, LNCS 915. 〈hal-01124466〉
  • Sandrine Blazy, Philippe Facon. SFAC, a tool for program comprehension by specialization. IEEE. 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 and symbolic computation for the understanding of Fortran programs. Springer Verlag. Advanced Information Systems Engineering 5th International Conference, CAiSE '93, 1993, Paris, France. 685, pp.184-198, Lecture Notes in Computer Science. 〈10.1007/3-540-56777-1〉. 〈inria-00165950〉
  • 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, 1993. 〈hal-01124468〉
  • 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, 1992. 〈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, Nov 1992, Orlando, USA, France. pp.18-26, 1992, 〈10.1109/ICSM.1992.242563〉. 〈inria-00143556〉

Chapitre d'ouvrage1 document

  • 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〉

Direction d'ouvrage, Proceedings, Dossier5 documents

  • Sandrine Blazy, Marsha Chechik. Verified Software: Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Toronto, Canada, July 17-18, 2016. Proceedings. Blazy, Sandrine and Chéchia, Marsha. 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. 〈sas2015.inria.fr〉. 〈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. INRIA. 2008. 〈hal-01125405〉
  • 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〉

HDR1 document

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