Skip to Main content Skip to Navigation

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 :
Complete list of metadatas
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:14:41 AM
Last modification on : Thursday, November 21, 2019 - 2:39:48 AM


Files produced by the author(s)


  • HAL Id : hal-02102116, version 1



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⟩



Record views


Files downloads