Bibliography¶
Description 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.
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. Proceedings of the 8th Conference on Real Numbers and Computers. 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. Proceedings of the 8th Conference on Real Numbers and Computers. 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. Proceedings of the 16th Calculemus Symposium. 59-74. Grand Bend, ON, Canada. 2009.
Claude-Pierre Jeannerod and Guillaume Revy. Optimizing correctly-rounded reciprocal square roots for embedded VLIW cores. Proceedings of the 43rd Asilomar Conference on Signals, Systems and Computers. 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. Proceedings of the 19th Symposium on Computer Arithmetic. 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. Proceedings of the 8th International Symposium on Code Generation and Optimization. 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. Proceedings of the 2nd NASA Formal Methods Symposium. 14-23. Washington DC, USA. 2010.
Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. Proceedings of the 5th International Joint Conference on Automated Reasoning. 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. Proceedings of the 20th Symposium on Computer Arithmetic. 233-242. Tübingen, Germany. 2011.
Claude-Pierre Jeannerod and Jingyan Jourdan-Lu. Simultaneous floating-point sine and cosine for VLIW integer processors. Proceedings of the 23rd International Conference on Application-Specific Systems, Architectures and Processors. 69-76. Delft, The Netherlands. 2012.
Olga Kupriianova and Christoph Lauter. Metalibm: A Mathematical Functions Code Generator. Proceedings of the 4th International Congress on Mathematical Software. 713-717. Seoul, Korea. 2014.