Difference between revisions of "Publications"
Jump to navigation
Jump to search
Xavier Leroy (talk | contribs) (→Conference papers:: Ajout 2e papier SAS13 et papier ITP13) |
|||
Line 11: | Line 11: | ||
===Conference papers:=== | ===Conference papers:=== | ||
− | * Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. '''A Formally-Verified C Compiler Supporting Floating-Point Arithmetic'''. In ''21st IEEE International Symposium on Computer Arithmetic'', IEEE Press, April 2013. [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'''. In ''ARITH, 21st IEEE International Symposium on Computer Arithmetic'', pages 107-115. IEEE Press, April 2013. [http://hal.inria.fr/hal-00743090 At HAL] |
− | * Sandrine Blazy | + | * Sandrine Blazy, Vincent Laporte, André Maronèze, and David Pichardie. '''Formal Verification of a C Value Analysis Based on Abstract Interpretation'''. In ''20th Static Analysis Symposium (SAS 2013)'', volume ? of Lecture Notes in Computer Science, pages ?-?. Springer, June 2013. [http://hal.inria.fr/hal-00812515 At HAL] |
+ | |||
+ | * Alexis Fouilhé, David Monniaux, and Michaël Périn. '''Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra'''. In ''20th Static Analysis Symposium (SAS 2013)'', volume ? of Lecture Notes in Computer Science, pages ?-?. Springer, June 2013. [http://hal.archives-ouvertes.fr/hal-00806990 At HAL] | ||
+ | |||
+ | * Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. '''Implementing hash-consed structures in Coq'''. In ''Interactive Theorem Proving (ITP 2013)''. Springer, July 2013. [http://hal.archives-ouvertes.fr/hal-00816672 At HAL] | ||
===Under submission:=== | ===Under submission:=== |
Revision as of 13:18, 17 May 2013
Contents
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, December 2012. At HAL
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
In 2013:
Conference papers:
- 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 Press, April 2013. At HAL
- Sandrine Blazy, Vincent Laporte, André Maronèze, and David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. In 20th Static Analysis Symposium (SAS 2013), volume ? of Lecture Notes in Computer Science, pages ?-?. Springer, June 2013. At HAL
- Alexis Fouilhé, David Monniaux, and Michaël Périn. Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. In 20th Static Analysis Symposium (SAS 2013), volume ? of Lecture Notes in Computer Science, pages ?-?. Springer, June 2013. At HAL
- Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. Implementing hash-consed structures in Coq. In Interactive Theorem Proving (ITP 2013). Springer, July 2013. At HAL