Skip to Main content Skip to Navigation

Generating certified properties for numerical expressions and their evaluations

Abstract : We present Gappa, a tool that can generate certified properties based on dyadic fractions, interval arithmetic and forward error analysis. Gappa operates on numerical expressions and on their evaluation on computers. For each property, Gappa generates a proof that can be checked with an automatic proof checker with the help of a companion library of verified facts. So far, Gappa generates proofs for either Coq and HOL Light and we have developed a large companion library for Coq dealing with the addition, multiplication, division, and square root, in fixed- and floating-point arithmetics. Gappa handles seamlessly additional properties expressed as interval properties or rewriting rules in order to establish more intricate results. Users can simultaneously provide bounds to be proved on expressions and ask Gappa to propose ones on other expressions. Recent work has proved that Gappa is perfectly adapted to the verification of small pieces of software. For larger pieces of software, Gappa can either be used to double check assertions produced by non verified tools or be invoked as needed by tools that handle loops and branches but miss the ability to handle possible effects of the accumulation and magnification of negligible errors.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas
Contributor : Marc Daumas <>
Submitted on : Monday, January 29, 2007 - 4:28:31 PM
Last modification on : Thursday, January 17, 2019 - 3:16:03 PM
Document(s) archivé(s) le : Tuesday, April 6, 2010 - 10:50:25 PM


Files produced by the author(s)




Marc Daumas, Guillaume Melquiond. Generating certified properties for numerical expressions and their evaluations. 2007. ⟨hal-00127769v1⟩



Record views


Files downloads