Difference between revisions of "Publications"
Jump to navigation
Jump to search
Xavier Leroy (talk | contribs) (MAJ publications) |
|||
| Line 22: | Line 22: | ||
* {{bibv|Braibant_Jourdan_Monniaux_ITP2013}} Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. '''Implementing hash-consed structures in Coq'''. In ''Interactive Theorem Proving (ITP 2013)'', volume 7998 of Lecture Notes in Computer Science, pages 477-483. Springer, July 2013. [http://hal.archives-ouvertes.fr/hal-00816672 At HAL] | * {{bibv|Braibant_Jourdan_Monniaux_ITP2013}} Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. '''Implementing hash-consed structures in Coq'''. In ''Interactive Theorem Proving (ITP 2013)'', volume 7998 of Lecture Notes in Computer Science, pages 477-483. Springer, July 2013. [http://hal.archives-ouvertes.fr/hal-00816672 At HAL] | ||
| + | |||
| + | ==In 2014== | ||
| + | |||
| + | ===Journal articles=== | ||
| + | |||
| + | * Gilles Barthe, Delphine Demange, David Pichardie. '''A formally verified SSA-based middle-end. Static Single Assignment meets CompCert'''. ACM Transactions on Programming Languages and Systems (TOPLAS), 36(1):article 4, March 2014. [http://dx.doi.org/10.1145/2579080 At publisher's] | ||
| + | |||
| + | ===Conference papers=== | ||
| + | |||
| + | * Sandrine Blazy, Vincent Laporte and David Pichardie. '''Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code'''. In ITP 2014: Interactive Theorem Proving. Lecture Notes in Computer Science, Springer, July 2014. To appear. | ||
| + | |||
| + | * Robbert Krebbers, Xavier Leroy and Freek Wiedijk. '''Formal C semantics: CompCert and the C standard'''. In ITP 2014: Interactive Theorem Proving. Lecture Notes in Computer Science, Springer, July 2014. To appear. | ||
==Under submission== | ==Under submission== | ||
| − | + | * Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. '''A Formally-Verified C Compiler Supporting Floating-Point Arithmetic''', submitted to a journal, Sept 2013. [http://hal.inria.fr/hal-00862689 At HAL] | |
| − | |||
| − | * Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. '''A Formally-Verified C Compiler Supporting Floating-Point Arithmetic''', submitted to | ||
| − | * Sylvie Boldo. '''How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound''', submitted to | + | * Sylvie Boldo. '''How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound''', submitted to a journal, Sept 2013. [http://hal.inria.fr/hal-00862653 At HAL] |
Revision as of 18:10, 31 March 2014
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
- [Boldo_et_al_ARITH21] 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 91-98. IEEE Press, April 2013. At HAL
- [Boldo_ARITH21] Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit. In ARITH, 21st IEEE International Symposium on Computer Arithmetic, pages 107-115. IEEE Press, April 2013. At HAL
- [Blazy_et_al_VSTTE2013] Sandrine Blazy, Vincent Laporte, André Maronèze, and David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. In VSTTE - Verified Software: Theories, Tools and Experiments, volume 8164 of Lecture Notes in Computer Science, pages 281-303. Springer, May 2013. At HAL
- [Blazy_et_al_SAS2013] Sandrine Blazy, 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 7935 of Lecture Notes in Computer Science, pages 324-344. Springer, June 2013. At HAL
- [Fouilhe_et_al_SAS2013] 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 7935 of Lecture Notes in Computer Science, pages 345-365. Springer, June 2013. At HAL
- [Braibant_Jourdan_Monniaux_ITP2013] Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. Implementing hash-consed structures in Coq. In Interactive Theorem Proving (ITP 2013), volume 7998 of Lecture Notes in Computer Science, pages 477-483. Springer, July 2013. At HAL
In 2014
Journal articles
- Gilles Barthe, Delphine Demange, David Pichardie. A formally verified SSA-based middle-end. Static Single Assignment meets CompCert. ACM Transactions on Programming Languages and Systems (TOPLAS), 36(1):article 4, March 2014. At publisher's
Conference papers
- Sandrine Blazy, Vincent Laporte and David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. In ITP 2014: Interactive Theorem Proving. Lecture Notes in Computer Science, Springer, July 2014. To appear.
- Robbert Krebbers, Xavier Leroy and Freek Wiedijk. Formal C semantics: CompCert and the C standard. In ITP 2014: Interactive Theorem Proving. Lecture Notes in Computer Science, Springer, July 2014. To appear.
Under submission
- Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, submitted to a journal, Sept 2013. At HAL
- Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound, submitted to a journal, Sept 2013. At HAL
