Difference between revisions of "Publications"
Jump to navigation
Jump to search
Xavier Leroy (talk | contribs) (Created page with "==In 2012:== ===Conference papers:=== * Valentin Robert and Xavier Leroy. '''A formally-verified alias analysis'''. In ''Certified Programs and Proofs (CPP 2012)'', volume 76...") |
|||
| Line 2: | Line 2: | ||
===Conference papers:=== | ===Conference papers:=== | ||
| − | * 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-27. Springer, 2012. [http://gallium.inria.fr/~xleroy/publi/alias-analysis.pdf PDF] | + | * {{bibv|Robert_Leroy_CPP2012}} 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-27. Springer, 2012. [http://gallium.inria.fr/~xleroy/publi/alias-analysis.pdf PDF] |
===Technical reports:=== | ===Technical reports:=== | ||
| − | * Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. '''The CompCert memory model, version 2'''. Research report RR-7987, INRIA, June 2012. [http://hal.inria.fr/hal-00703441 At HAL] | + | * {{bibv|leroy:hal-00703441}} Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. '''The CompCert memory model, version 2'''. Research report RR-7987, INRIA, June 2012. [http://hal.inria.fr/hal-00703441 At HAL] |
===Under submission:=== | ===Under submission:=== | ||
* Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. '''A Formally-Verified C Compiler Supporting Floating-Point Arithmetic'''. September 2012. [http://hal.inria.fr/hal-00743090 At HAL] | * Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. '''A Formally-Verified C Compiler Supporting Floating-Point Arithmetic'''. September 2012. [http://hal.inria.fr/hal-00743090 At HAL] | ||
Revision as of 10:00, 23 October 2012
In 2012:
Conference papers:
- [Robert_Leroy_CPP2012] 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-27. Springer, 2012. PDF
Technical reports:
- [leroy:hal-00703441] Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012. At HAL
Under submission:
- Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. September 2012. At HAL
