HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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 metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 9:28:52 PM
Last modification on : Friday, February 4, 2022 - 3:23:38 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:49:18 PM


  • HAL Id : inria-00070739, version 1



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⟩



Record views


Files downloads