PhD and Habilitation theses

[1] Sandrine Blazy. Sémantiques formelles. Habilitation à diriger les recherches, Université Évry Val d'Essone, October 2008. [ bib | HAL archive | Local copy ]
[2] Zaynah Dargaye. Vérification formelle d'un compilateur pour langages fonctionnels. PhD thesis, Université Paris 7 Diderot, July 2009. [ bib | HAL archive ]
[3] Jean-Baptise Tristan. Formal verification of translation validators. PhD thesis, Université Paris 7 Diderot, November 2009. [ bib | HAL archive ]
[4] Jacques-Henri Jourdan. Verasco: a Formally Verified C Static Analyzer. Phd thesis, Université Paris 7 Diderot, May 2016. [ bib | HAL archive ]

Articles in journals

[1] Sandrine Blazy. Comment gagner confiance en C ? Technique et Science Informatiques, 26(9):1195--1200, 2007. [ bib | HAL archive | Local copy ]
[2] Xavier Leroy and Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 41(1):1--31, 2008. [ bib | HAL archive | Local copy | At publisher's ]
[3] Laurence Rideau, Bernard Paul Serpette, and Xavier Leroy. Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning, 40(4):307--326, 2008. [ bib | HAL archive | Local copy | At publisher's ]
[4] Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284--304, 2009. [ bib | HAL archive | Local copy | At publisher's ]
[5] Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363--446, 2009. [ bib | HAL archive | Local copy | At publisher's ]
[6] Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263--288, 2009. [ bib | HAL archive | Local copy | At publisher's ]
[7] Zaynah Dargaye and Xavier Leroy. A verified framework for higher-order uncurrying optimizations. Higher-Order and Symbolic Computation, 22(3):199--231, 2009. [ bib | Local copy | At publisher's ]
[8] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107--115, 2009. [ bib | HAL archive | Local copy | At publisher's ]
[9] Xavier Leroy. Comment faire confiance à un compilateur? La Recherche, 440, April 2010. Les cahiers de l'INRIA. [ bib | Local copy | At publisher's ]
[10] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified compilation of floating-point computations. Journal of Automated Reasoning, 54(2):135--163, 2015. [ bib | Local copy | At publisher's ]

Proceedings of international refereed conferences and workshops

[1] Sandrine Blazy and Xavier Leroy. Formal verification of a memory model for C-like imperative languages. In International Conference on Formal Engineering Methods (ICFEM 2005), volume 3785 of Lecture Notes in Computer Science, pages 280--299. Springer, 2005. [ bib | HAL archive | Local copy | At publisher's ]
[2] Yves Bertot, Benjamin Grégoire, and Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Types for Proofs and Programs, Workshop TYPES 2004, volume 3839 of Lecture Notes in Computer Science, pages 66--81. Springer, 2006. [ bib | HAL archive | Local copy | At publisher's ]
[3] Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd ACM symposium on Principles of Programming Languages, pages 42--54. ACM Press, 2006. [ bib | HAL archive | Local copy | At publisher's ]
[4] Xavier Leroy. Coinductive big-step operational semantics. In European Symposium on Programming (ESOP'06), volume 3924 of Lecture Notes in Computer Science, pages 54--68. Springer, 2006. [ bib | HAL archive | Local copy | At publisher's ]
[5] Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In FM 2006: Int. Symp. on Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 460--475. Springer, 2006. [ bib | HAL archive | Local copy | At publisher's ]
[6] Andrew W. Appel and Sandrine Blazy. Separation logic for small-step Cminor. In Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science, pages 5--21. Springer, 2007. [ bib | HAL archive | Local copy | At publisher's ]
[7] Sandrine Blazy. Experiments in validating formal semantics for C. In Proceedings of the C/C++ Verification Workshop, pages 95--102. Technical report ICIS-R07015, Radboud University Nijmegen, 2007. [ bib | HAL archive | Local copy ]
[8] Zaynah Dargaye and Xavier Leroy. Mechanized verification of CPS transformations. In Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, volume 4790 of Lecture Notes in Artificial Intelligence, pages 211--225. Springer, 2007. [ bib | HAL archive | Local copy | At publisher's ]
[9] Richard Bonichon, David Delahaye, and Damien Doligez. Zenon: an extensible automated theorem prover producing checkable proofs. In Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, volume 4790 of Lecture Notes in Artificial Intelligence, pages 151--165. Springer, 2007. [ bib | HAL archive | Local copy | At publisher's ]
[10] Andrew W. Appel and Xavier Leroy. A list-machine benchmark for mechanized metatheory (extended abstract). In Proc. Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP'06), volume 174/5 of Electronic Notes in Computer Science, pages 95--108, 2007. [ bib | HAL archive | Local copy | At publisher's ]
[11] Jean-Baptiste Tristan and Xavier Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. In Proceedings of the 35th ACM Symposium on Principles of Programming Languages (POPL'08), pages 17--27. ACM Press, January 2008. [ bib | HAL archive | Local copy | At publisher's ]
[12] Yves Bertot and Vladimir Komendantsky. Fixed point semantics and partial recursion in Coq. In 10th int. ACM SIGPLAN conference on Principles and Practice of Declarative Programming (PPDP 2008), pages 89--96. ACM Press, 2008. [ bib | HAL archive | At publisher's ]
[13] Pierre Letouzey. Extraction in Coq: An overview. In Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008, volume 5028 of Lecture Notes in Computer Science, pages 359--369. Springer, 2008. [ bib | HAL archive | At publisher's ]
[14] Jean-Baptiste Tristan and Xavier Leroy. Verified validation of Lazy Code Motion. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'09), pages 316--326, 2009. [ bib | HAL archive | Local copy | At publisher's ]
[15] Sandrine Blazy and Benoît Robillard. Live-range unsplitting for faster optimal coalescing. In Proceedings of the ACM SIGPLAN/SIGBED 2009 conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009), pages 70--79. ACM Press, 2009. [ bib | HAL archive | Local copy | At publisher's ]
[16] Jean-Baptiste Tristan and Xavier Leroy. A simple, verified validator for software pipelining. In Proceedings of the 37th ACM Symposium on Principles of Programming Languages (POPL'10), pages 83--92. ACM Press, 2010. [ bib | Local copy | At publisher's ]
[17] Silvain Rideau and Xavier Leroy. Validating register allocation and spilling. In Compiler Construction (CC 2010), volume 6011 of Lecture Notes in Computer Science, pages 224--243. Springer, 2010. [ bib | Local copy | At publisher's ]
[18] Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. Towards optimizing certified compilation in flight control software. In Workshop on Predictability and Performance in Embedded Systems (PPES 2011), volume 18 of OpenAccess Series in Informatics, pages 59--68. Dagstuhl Publishing, 2011. [ bib | Local copy | At publisher's ]
[19] Xavier Leroy. Verified squared: does critical software deserve verified tools? In 38th symposium Principles of Programming Languages, pages 1--2. ACM Press, 2011. Abstract of invited lecture. [ bib | Local copy | At publisher's ]
[20] Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. In Embedded Real Time Software and Systems (ERTS 2012), 2012. [ bib | Local copy ]
[21] Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. Validating LR(1) parsers. In Programming Languages and Systems -- 21st European Symposium on Programming, ESOP 2012, volume 7211 of Lecture Notes in Computer Science, pages 397--416. Springer, 2012. [ bib | Local copy | At publisher's ]
[22] Xavier Leroy. Mechanized semantics for compiler verification. In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems, 10th Asian Symposium, APLAS 2012, volume 7705 of Lecture Notes in Computer Science, pages 386--388. Springer, 2012. Abstract of invited talk. [ bib | Local copy | At publisher's ]
[23] Valentin Robert and Xavier Leroy. A formally-verified alias analysis. In Certified Programs and Proofs (CPP 2012), volume 7679 of Lecture Notes in Computer Science, pages 11--26. Springer, 2012. [ bib | Local copy | At publisher's ]
[24] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In ARITH, 21st IEEE International Symposium on Computer Arithmetic, pages 107--115. IEEE Computer Society Press, 2013. [ bib | Local copy ]
[25] Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In POPL 2015: 42nd symposium Principles of Programming Languages, pages 247--259. ACM Press, 2015. [ bib | Local copy | At publisher's ]
[26] Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. Compcert -- a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems. SEE, 2016. [ bib | HAL archive | Local copy ]
[27] Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, and Christian Ferdinand. Closing the gap -- the formally verified optimizing compiler CompCert. In SSS'17: Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium, pages 163--180. CreateSpace, 2017. [ bib | HAL archive | At publisher's ]
[28] Timothy Bourke, Lélio Brun, Pierre Évariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. A formally verified compiler for Lustre. In PLDI 2017: Programming Language Design and Implementation, pages 586--601. ACM Press, 2017. [ bib | HAL archive | Local copy | At publisher's ]
[29] 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. In ERTS 2018: Embedded Real Time Software and Systems. SEE, January 2018. [ bib | HAL archive | Local copy ]
[30] Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, and Simon Wegener. Embedded program annotations for WCET analysis. In WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis, volume 63 of OASIcs. Dagstuhl Publishing, July 2018. [ bib | DOI | HAL archive | At publisher's ]

Proceedings of national conferences and workshops

[1] Zaynah Dargaye. Décurryfication certifiée. In Journées Francophones des Langages Applicatifs (JFLA'07), pages 119--134. INRIA, 2007. [ bib | HAL archive | Local copy ]
[2] Sandrine Blazy, Benoît Robillard, and Eric Soutif. Coloration avec préférences dans les graphes triangulés. In Journées Graphes et Algorithmes (JGA'07), November 2007. [ bib | Local copy ]
[3] Sandrine Blazy, Benoît Robillard, and Eric Soutif. Vérification formelle d'un algorithme d'allocation de registres par coloration de graphes. In Journées Francophones des Langages Applicatifs (JFLA'08), pages 31--46, Étretat, France, January 2008. [ bib | HAL archive | Local copy ]
[4] Sandrine Blazy, Benoît Robillard, and Éric Soutif. Coloration avec préférences: complexité, inégalités valides et vérification formelle. In ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, 2008. [ bib | HAL archive ]
[5] Stéphane Glondu. Extraction certifiée dans Coq-en-Coq. In Journées Francophones des Langages Applicatifs (JFLA'09), pages 105--118. INRIA, 2009. [ bib | HAL archive | Local copy ]

Book chapters

[1] Yves Bertot. Theorem proving support in programming language semantics. In Y. Bertot, G. Huet, J.-J. Lévy, and G. Plotkin, editors, From Semantics to Computer Science -- Essays in Honour of Gilles Kahn, pages 337--362. Cambridge University Press, 2009. [ bib | At publisher's ]
[2] Yves Bertot. Structural abstract interpretation: A formal study using Coq. In Ana Bove and Jorge Sousa Pinto, editors, Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, volume 5520 of Lecture Notes in Computer Science, pages 153--194. Springer, 2009. [ bib | HAL archive | At publisher's ]
[3] Xavier Leroy. Mechanized semantics. In Logics and languages for reliability and security, volume 25 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 195--224. IOS Press, 2010. [ bib | Local copy | At publisher's ]
[4] Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model. In Andrew W. Appel, editor, Program Logics for Certified Compilers. Cambridge University Press, April 2014. [ bib | Local copy ]

Technical reports

[1] Andrew W. Appel and Xavier Leroy. A list-machine benchmark for mechanized metatheory. Research report 5914, INRIA, 2006. [ bib | HAL archive ]
[2] Andrew W. Appel and Sandrine Blazy. Separation logic for small-step Cminor (extended version). Research report 6138, INRIA, 2007. 29 pages. [ bib | HAL archive ]
[3] Yves Bertot. Theorem proving support in programming language semantics. Research report 6242, INRIA, 2007. [ bib | HAL archive ]
[4] Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012. [ bib | Local copy ]

Preprints

[1] Yves Bertot. Extending the calculus of constructions with Tarski's fix-point theorem. 2006. [ bib | HAL archive ]