# Publications

From VERASCO

## 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 HAL At publisher's

- Thomas Braibant, Jacques-Henri Jourdan, David Monniaux.
**Implementing and reasoning about hash-consed data structures in Coq**. Journal of Automated Reasoning (JAR), 53(3):271-304, 2014. At HAL At publisher's

- Pierre Roux.
**Innocuous Double Rounding of Basic Arithmetic Operations**. Journal of Formalized Reasoning, 7(1):131-142, 2014. At HAL. 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*, pages 128-143. Lecture Notes in Computer Science 8558, Springer, July 2014. At HAL At publisher's

- Robbert Krebbers, Xavier Leroy and Freek Wiedijk.
**Formal C semantics: CompCert and the C standard**. In*ITP 2014: Interactive Theorem Proving*, pages 543-548. Lecture Notes in Computer Science 8558, Springer, July 2014. At HAL At publisher's

- Alexis Fouilhe and Sylvain Boulmé.
**A certifying frontend for (sub)polyhedral abstract domains**. In*Verified Software: Theories, Tools and Experiments (VSTTE) 2014*, pages 200-215. Lecture Notes in Computer Science 8471, Springer, July 2014. At HAL At publisher's

### Workshops without proceedings

- Alexis Fouilhe, Sylvain Boulmé and Michaël Périn.
**Modular and lightweight certification of polyhedral abstract domain**. TYPES meeting, May 2014. Abstract

- Xavier Leroy.
**Formal verification of a static analyzer: abstract interpretation in type theory**. TYPES meeting, May 2014. At HAL

### Book chapters

- Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart.
**The CompCert memory model**. In Andrew W. Appel,*Program Logics for Certified Compilers*, pp. 237-271. Cambridge University Press, April 2014. At publisher's

## In 2015

### PhD theses

- Alexis Fouilhé.
**Revisiting the abstract domain of polyhedra : constraints-only representation and formal proof**. PhD thesis, Université Grenoble Alpes, October 2015. At HAL.

- Vincent Laporte.
**Verified static analyzes for low-level languages**. PhD thesis, Université Rennes 1, November 2015. At HAL.

### Journal articles

- Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond.
**Verified Compilation of Floating-Point Computations**. Journal of Automated Reasoning (JAR), 54(2):135-163, 2015. At HAL At publisher's

- Érik Martin-Dorel and Guillaume Melquiond.
**Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq**. Journal of Automated Reasoning (JAR), 2015. At HAL At publisher's

### Conference papers

- Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie.
**A formally-verified C static analyzer**. In*POPL 2015: 42nd symposium Principles of Programming Languages*, pp 247-259. ACM Press, January 2015. At HAL At publisher's

- Sandrine Blazy, Andre Maroneze, and David Pichardie.
**Verified Validation of Program Slicing**. In*CPP 2015: conference on Certified Programs and Proofs*, pp 109-117. ACM Press, January 2015. at HAL At publisher's

- Sylvie Boldo.
**Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number**. In*Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification*, Electronic Notes in Theoretical Computer Science, pages 50-55, Seattle, WA, USA, April 2015. At HAL

- Sandrine Blazy, Delphine Demange, David Pichardie.
**Validating Dominator Trees for a Fast, Verified Dominance Test**. In*ITP 2015: 6th international conference on Interactive Theorem Proving*, pp 84-99. Lecture Notes in Computer Science 9236, Springer, August 2015. At HAL. At publisher's.

- Sylvain Boulmé, Alexandre Maréchal.
**Refinement to certify abstract interpretations, illustrated on linearization for polyhedra**. In*ITP 2015: 6th international conference on Interactive Theorem Proving*, pp 100-116. Lecture Notes in Computer Science 9236, Springer, August 2015. At HAL At publisher's.

- Sylvie Boldo.
**Formal Verification of Programs Computing the Floating-Point Average**. In*ICFEM 2015: 17th International Conference on Formal Engineering Methods*, pp 17-32. Lecture Notes in Computer Science 9407, Springer, November 2015. At HAL.

## In 2016

### PhD thesis

- Jacques-Henri Jourdan.
**Verasco: a formally verified C static analyzer**. PhD thesis, Université Paris Diderot (Paris 7), May 2016. At HAL. Local copy.

### Journal articles

- Sandrine Blazy, Vincent Laporte, and David Pichardie.
**Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code**. Journal of Automated Reasoning (JAR), 56(3):283-308, 2016. At HAL. At publisher's

### Conference papers

- Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, Christian Ferdinand.
**CompCert - A Formally Verified Optimizing Compiler**. In*ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress*, January 2016. At HAL At publisher's.

- Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michaël Périn.
**Polyhedral Approximation of Multivariate Polynomials using Handelman's Theorem**. In*VMCAI 2016: International Conference on Verification, Model Checking, and Abstract Interpretation*, January 2016. At HAL. At publisher's

- Sandrine Blazy, Vincent Laporte, David Pichardie.
**An Abstract Memory Functor for Verified C Static Analyzers**. In*ICFP 2016: 21th International Conference on Functional Programming*, ACM Press, September 2016. At HAL. At publisher's

- Jacques-Henri Jourdan.
**Sparsity Preserving Algorithms for Octagons**. In*NSAD 2016: Numerical and symbolic abstract domains workshop*, September 2016, Edinburgh, United Kingdom. Electr. Notes Theor. Comput. Sci. 331: 57-70 (2017). At HAL. At publisher's