Difference between revisions of "Publications"

From VERASCO
Jump to navigation Jump to search
m
m
Line 1: Line 1:
==In 2012:==
+
==In 201:==
  
===Conference papers:===
+
===Conference papers===
 
* {{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, December 2012. [http://hal.inria.fr/hal-00773109 At HAL]
 
* {{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, December 2012. [http://hal.inria.fr/hal-00773109 At HAL]
  
===Technical reports:===
+
===Technical reports===
 
* {{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]
 
* {{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]
  
  
==In 2013:==
+
==In 2013==
  
===Conference papers:===
+
===Conference papers===
 
* {{bibv|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.  [http://hal.inria.fr/hal-00743090 At HAL]
 
* {{bibv|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.  [http://hal.inria.fr/hal-00743090 At HAL]
  
Line 24: Line 24:
  
  
==Under submission:==
+
==Under submission==
  
 
* Gilles Barthe, Delphine Demange, David Pichardie. '''A formally verified SSA-based middle-end. Static Single Assignment meets CompCert''', submitted to ACM TOPLAS, March 2013.
 
* Gilles Barthe, Delphine Demange, David Pichardie. '''A formally verified SSA-based middle-end. Static Single Assignment meets CompCert''', submitted to ACM TOPLAS, March 2013.

Revision as of 16:49, 15 September 2013

In 201:

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 ? of Lecture Notes in Computer Science, pages ?-?. 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 ? of Lecture Notes in Computer Science, pages ?-?. 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 ? of Lecture Notes in Computer Science, pages ?-?. 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). Springer, July 2013. At HAL


Under submission

  • Gilles Barthe, Delphine Demange, David Pichardie. A formally verified SSA-based middle-end. Static Single Assignment meets CompCert, submitted to ACM TOPLAS, March 2013.
  • Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, submitted to IEEE Trans. Comp., Sept 2013.
  • Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit, submitted to IEEE Trans. Comp., Sept 2013.