Generating formally certified bounds on values and round-off errors

Marc Daumas 1 Guillaume Melquiond 1
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
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 :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00070739
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 9:28:52 PM
Last modification on : Wednesday, April 17, 2019 - 4:08:00 PM
Long-term archiving on : Sunday, April 4, 2010 - 9:49:18 PM

Identifiers

  • HAL Id : inria-00070739, version 1

Collections

Citation

Marc Daumas, Guillaume Melquiond. Generating formally certified bounds on values and round-off errors. Real Numbers and Computers, 2004, Dagstuhl, Germany. pp.55-70. ⟨inria-00070739⟩

Share

Metrics

Record views

272

Files downloads

307