Certifying the Floating-Point Implementation of an Elementary Function Using Gappa

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...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computers 2011-02, Vol.60 (2), p.242-253
Main Authors: de Dinechin, Florent, Lauter, C, Melquiond, G
Format: Article
Language:English
Subjects:
Accuracy
Approximation algorithms
Approximation error
Automation
Computer Arithmetic
Computer Science
Correctness proofs
elementary function approximation
error analysis
Errors
Floating point arithmetic
Image reconstruction
Interval arithmetic
Mathematical analysis
Mathematical models
Polynomials
Program processors
Proving
Studies
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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, due 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 paper demonstrates the practical use of this tool for a widely used class of floating-point programs: implementations of elementary functions in a mathematical library.
ISSN:0018-9340
1557-9956
DOI:10.1109/TC.2010.128