Generating formally certified bounds on values and round-off errors.

Abstract : We present a new tool that generates bounds on the values and the round-off errors of programs using floating point operations. The tool is based on forward error analysis and interval arithmetic. The novelty of our tool is that it produces a formal proof of the bounds that can be checked independently using an automatic proof checker such as Coq and a complete model of floating point arithmetic. For the first time ever, we can easily certify that simple numerical programs such as the ones usually found in real time applications do not overflow and that round-off errors are below acceptable thresholds. Such level of quality should be compulsory on safety critical applications. As our tool is easy to handle, it could also be used for many pieces of software.
Document type :
Reports
Complete list of metadatas

https://hal-lara.archives-ouvertes.fr/hal-02102116
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:14:41 AM
Last modification on : Sunday, April 28, 2019 - 1:23:05 AM

File

RR2004-36.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102116, version 1

Collections

Citation

Marc Daumas, Guillaume Melquiond. Generating formally certified bounds on values and round-off errors.. [Research Report] LIP RR-2004-36, Laboratoire de l'informatique du parallélisme. 2004, 2+24p. ⟨hal-02102116⟩

Share

Metrics

Record views

10

Files downloads

24