Skip to Main content Skip to Navigation


...
hal-01512286v1  Conference papers
Timothy BourkeLélio BrunPierre-Evariste DagandXavier LeroyMarc Pouzet et al.  A Formally Verified Compiler for Lustre
PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, Jun 2017, Barcelone, Spain
...
hal-02392159v2  Books
Xavier Leroy. Software, between mind and matter
Collège de France, 2020, Inaugural lecture at Collège de France
hal-02370113v1  Books
Xavier Leroy. Le logiciel, entre l'esprit et la matière
Fayard, 284, 2019, Leçons inaugurales du Collège de France, 978-2-213-71241-3
hal-02392114v1  Conference papers
Xavier Leroy. In Search of Software Perfection
BOB Summer 2019 Konferenz, Aug 2019, Berlin, Germany
...
inria-00289549v1  Conference papers
Yves BertotBenjamin GrégoireXavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis
Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. pp.66-81, ⟨10.1007/11617990⟩
...
hal-01848686v1  Conference papers
Bernhard SchommerChristoph CullmannGernot GebhardXavier LeroyMichael Schmidt et al.  Embedded Program Annotations for WCET Analysis
WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis, Jul 2018, Barcelona, Spain. ⟨10.4230/OASIcs.WCET.2018.8⟩
...
hal-01238879v1  Conference papers
Xavier LeroySandrine BlazyDaniel KästnerBernhard SchommerMarkus Pister et al.  CompCert - A Formally Verified Optimizing Compiler
ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, Jan 2016, Toulouse, France
hal-00905435v1  Book sections
Xavier LeroyAndrew W. AppelSandrine BlazyGordon Stewart. The CompCert memory model
Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010
...
hal-01078386v1  Conference papers
Jacques-Henri JourdanVincent LaporteSandrine BlazyXavier LeroyDavid Pichardie. A formally-verified C static analyzer
POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩
...
hal-01643290v1  Conference papers
Daniel KästnerJörg BarrhoUlrich WünscheMarc SchlicklingBernhard Schommer et al.  CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler
ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems, 3AF, SEE, SIE, Jan 2018, Toulouse, France. pp.1-9
...
inria-00077921v1  Conference papers
Sandrine BlazyXavier Leroy. Formal verification of a memory model for C-like imperative languages
ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. pp.280-299, ⟨10.1007/11576280⟩
...
hal-00862689v3  Journal articles
Sylvie BoldoJacques-Henri JourdanXavier LeroyGuillaume Melquiond. Verified Compilation of Floating-Point Computations
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩
...
inria-00415865v1  Conference papers
Jean-Baptiste TristanXavier Leroy. Verified Validation of Lazy Code Motion
ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), Jun 2009, Dublin, Ireland. pp.316-326, ⟨10.1145/1542476.1542512⟩
...
hal-01059423v1  Conference papers
Xavier Leroy. Formal proofs of code generation and verification tools
SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. pp.1-4, ⟨10.1007/978-3-319-10431-7_1⟩
...
hal-00773109v1  Conference papers
Valentin RobertXavier Leroy. A formally-verified alias analysis
CPP 2012 - Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. pp.11-26, ⟨10.1007/978-3-642-35308-6_5⟩
...
hal-00703441v1  Reports
Xavier LeroyAndrew AppelSandrine BlazyGordon Stewart. The CompCert Memory Model, Version 2
[Research Report] RR-7987, INRIA. 2012, pp.26
...
hal-01077321v1  Conference papers
Jacques-Henri JourdanFrançois PottierXavier Leroy. Validating LR(1) Parsers
ESOP 2012 - Programming Languages and Systems - 21st European Symposium on Programming, Mar 2012, Tallinn, Estonia. pp.397-416, ⟨10.1007/978-3-642-28869-2_20⟩
...
inria-00289540v1  Conference papers
Jean-Baptiste TristanXavier Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations
35th ACM Symposium on Principles of Programming Languages (POPL 2008), ACM, Jan 2008, San Francisco, United States. pp.17-27, ⟨10.1145/1328438.1328444⟩
...
inria-00309010v1  Journal articles
Xavier LeroyHervé Grall. Coinductive big-step operational semantics
Information and Computation, Elsevier, 2009, 207 (2), pp.284-304. ⟨10.1016/j.ic.2007.12.004⟩
...
inria-00106401v1  Conference papers
Sandrine BlazyZaynah DargayeXavier Leroy. Formal Verification of a C Compiler Front-end
FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. pp.460-475, ⟨10.1007/11813040_31⟩
...
hal-00981212v1  Conference papers
Robbert KrebbersXavier LeroyFreek Wiedijk. Formal C semantics: CompCert and the C standard
ITP 2014: Fifth conference on Interactive Theorem Proving, Jul 2014, Vienna, Austria. pp.543-548, ⟨10.1007/978-3-319-08970-6_36⟩
...
hal-00674174v1  Conference papers
Tahina RamananandroGabriel dos ReisXavier Leroy. Formal verification of object layout for C++ multiple inheritance
POPL'11 - 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, Jan 2011, Austin, TX, United States. pp.67-79, ⟨10.1145/1926385.1926395⟩
...
hal-00653367v1  Conference papers
Ricardo Bedin FrançaSandrine BlazyDenis Favre-FelixXavier LeroyMarc Pantel et al.  Formally verified optimizing compilation in ACG-based flight control software
ERTS2 2012: Embedded Real Time Software and Systems, AAAF, SEE, Feb 2012, Toulouse, France