Publications

From VERASCO
Revision as of 11:42, 2 February 2013 by Xavier Leroy (talk | contribs) (ARITH 21 paper accepted. CPP 2012 paper available on HAL.)
Jump to navigation Jump to search

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 21st IEEE International Symposium on Computer Arithmetic, IEEE Press, April 2013. At HAL

Under submission: