Certifying the floating-point implementation of an elementary function using Gappa

Florent De Dinechin 1, 2 Christoph Lauter 3 Guillaume Melquiond 4, 5
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
4 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : High confidence in floating-point programs requires proving numerical properties of final and intermediate values. One may need to guarantee that a value stays within some range, or that the error relative to some ideal value is well bounded. This certification may require a time-consuming proof for each line of code, and it is usually broken by the smallest change to the code, e.g. for maintenance or optimization purpose. Certifying floating-point programs by hand is therefore very tedious and error-prone. The Gappa proof assistant is designed to make this task both easier and more secure, thanks to the following novel features. It automates the evaluation and propagation of rounding errors using interval arithmetic. Its input format is very close to the actual code to validate. It can be used incrementally to prove complex mathematical properties pertaining to the code. It generates a formal proof of the results, which can be checked independently by a lower-level proof assistant like Coq. Yet it does not require any specific knowledge about automatic theorem proving, and thus is accessible to a wide community. This article demonstrates the practical use of this tool for a widely used class of floating-point programs: implementations of elementary functions in a mathematical library.
Document type :
Journal articles
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2011, 60 (2), pp.242-253. 〈10.1109/TC.2010.128〉
Liste complète des métadonnées

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/ensl-00200830
Contributor : Guillaume Melquiond <>
Submitted on : Monday, November 8, 2010 - 3:35:24 PM
Last modification on : Wednesday, October 18, 2017 - 1:54:03 PM
Document(s) archivé(s) le : Friday, October 26, 2012 - 3:16:47 PM

File

10-tc.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Florent De Dinechin, Christoph Lauter, Guillaume Melquiond. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2011, 60 (2), pp.242-253. 〈10.1109/TC.2010.128〉. 〈ensl-00200830v2〉

Share

Metrics

Record views

520

Document downloads

292