Bibliography

Descriptions of Gappa

Marc Daumas and Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. ACM Transactions on Mathematical Software. 37(1):1-20. 2010.

Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. Handbook of Floating-Point Arithmetic. Birkhäuser, 2010.

Sylvie Boldo and Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. ISTE Press, 2017.

Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, and Serge Torres, Handbook of Floating-Point Arithmetic, 2nd edition. Birkhäuser, 2018.

Sylvie Boldo and Guillaume Melquiond. Some formal tools for computer arithmetic: Flocq and Gappa. 28th IEEE International Symposium on Computer Arithmetic. 2021.

Applications of Gappa

Guillaume Melquiond and Sylvain Pion. Formally certified floating-point filters for homogeneous geometric predicates. Theoretical Informatics and Applications. 41(1):57-70. 2007.

Arnaud Tisserand. High-performance hardware operators for polynomial evaluation. International Journal of High Performance Systems Architecture. 1(1):14-23. 2007.

Christoph Lauter and Florent de Dinechin. Optimizing polynomials for floating-point implementation. 8th Conference on Real Numbers and Computers, pp 7-16. Santiago de Compostella, Spain, 2008.

Sylvie Boldo, Marc Daumas, and Pascal Giorgi. Formal proof for delayed finite field arithmetic using floating point operators. 8th Conference on Real Numbers and Computers, pp 113-122. Santiago de Compostella, Spain, 2008.

Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for certifying floating-point programs. 16th Calculemus Symposium, pp 59-74. Grand Bend, ON, Canada, 2009.

Claude-Pierre Jeannerod and Guillaume Revy. Optimizing correctly-rounded reciprocal square roots for embedded VLIW cores. 43rd Asilomar Conference on Signals, Systems and Computers, pp 731-735. Pacific Grove, CA, USA, 2009.

Claude-Pierre Jeannerod, Hervé Knochel, Christophe Monat, Guillaume Revy, and Gilles Villard. A new binary floating-point division algorithm and its software implementation on the ST231 processor. 19th IEEE Symposium on Computer Arithmetic, pp 95-103. Portland, OR, USA, 2009.

Michael D. Linderman, Matthew Ho, David L. Dill, Teresa H. Meng, Garry P. Nolan. Towards program optimization through automated analysis of numerical precision. 8th International Symposium on Code Generation and Optimization, pp 230-237. Toronto, ON, Canada, 2010.

Vincent Lefèvre, Philippe Théveny, Florent de Dinechin, Claude-Pierre Jeannerod, Christophe Mouilleron, David Pfannholzer, and Nathalie Revol. LEMA: towards a language for reliable arithmetic. ACM SIGSAM Bulletin. 44(1/2):41-52. 2010.

Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. 2nd NASA Formal Methods Symposium, pp 14-23. Washington DC, USA, 2010.

Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. 5th International Joint Conference on Automated Reasoning, pp 127-141. Edinburgh, Scotland, 2010.

Claude-Pierre Jeannerod, Hervé Knochel, Christophe Monat, and Guillaume Revy. Computing floating-point square roots via bivariate polynomial evaluation. IEEE Transactions on Computers. 60(2):214-227. 2011.

Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers. 60(2):242-253. 2011.

Christophe Mouilleron and Guillaume Revy. Automatic generation of fast and certified code for polynomial evaluation. 20th Symposium on Computer Arithmetic, pp 233-242. Tübingen, Germany, 2011.

Claude-Pierre Jeannerod and Jingyan Jourdan-Lu. Simultaneous floating-point sine and cosine for VLIW integer processors. 23rd International Conference on Application-Specific Systems, Architectures and Processors, pp 69-76. Delft, The Netherlands, 2012.

Olga Kupriianova and Christoph Lauter. Metalibm: A mathematical functions code generator. 4th International Congress on Mathematical Software, pp 713-717. Seoul, Korea, 2014.

Sylvie Boldo. Formal verification of programs computing the floating-point average. 17th International Conference on Formal Engineering Methods, pp 17-32. Paris, France, 2015.

Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off error analysis of explicit one-step numerical integration methods. 24th IEEE Symposium on Computer Arithmetic, pp 82-89. London, UK, 2017.

Guillaume Melquiond and Raphaël Rieu-Helft. Formal verification of a state-of-the-art integer square root.. 26th IEEE Symposium on Computer Arithmetic, pp 183-186. Kyoto, Japan, 2019.

David Monniaux and Alice Pain. Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic. 29th IEEE Symposium on Computer Arithmetic, pp 128-132. 2022.

Paul Geneau de Lamarlière, Guillaume Melquiond, and Florian Faissole. Slimmer formal proofs for mathematical libraries. 30th IEEE International Symposium on Computer Arithmetic, pp 32-35. Portland, OR, USA, 2023.

Simon Tatham. Formally verifying a floating-point division routine with Gappa. ARM, 2025.

Tom Hubrecht and Guillaume Melquiond. Verifying code that uses error-free transformations. 33rd IEEE International Symposium on Computer Arithmetic. Fulda, Germany, 2026.

Paul Zimmermann. The GNU libc atanh is correctly rounded. 33rd IEEE International Symposium on Computer Arithmetic. Fulda, Germany, 2026.

Nicolas Brisebarre, Tom Hubrecht, Christoph Lauter, Jean-Michel Muller, and Kristalys Ruiz-Rohena. Correctly rounded vector implementation of the exponential function in binary64 arithmetic. 33rd IEEE International Symposium on Computer Arithmetic. Fulda, Germany, 2026.