Skip to Main content Skip to Navigation
New interface
Journal articles

Certification of bounds on expressions involving rounded operators

Marc Daumas 1, 2 Guillaume Melquiond 3, 4 
3 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Gappa is a tool designed to formally verify the correctness of numerical softwares and hardwares. It uses interval arithmetic and forward error analysis to bound mathematical expressions that involve rounded as well as exact operators. It then generates a theorem and its proof for each verified enclosure. This proof can be automatically checked with a proof assistant, such as Coq or HOL Light. It relies on the facts of a large companion library we have developed. This Coq library provides theorems dealing with addition, multiplication, division, and square root, for both fixed- and floating-point arithmetics. Gappa uses multiple-precision dyadic fractions for the endpoints of intervals and performs forward error analysis on rounded operators when necessary. When asked, Gappa reports the best bounds it is able to reach for a given expression in a given context. This feature can be used to identify where the set of facts and automatic techniques implemented in Gappa becomes insufficient. Gappa handles seamlessly additional properties expressed as interval properties or rewriting rules in order to establish more intricate bounds. Recent work showed that Gappa is suited to discharge proof obligations generated for small pieces of software. They may be produced by third-party tools and the first applications of Gappa use proof obligations written by designers or obtained from traces of execution.
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download
Contributor : Guillaume Melquiond Connect in order to contact the contributor
Submitted on : Tuesday, November 9, 2010 - 1:43:22 PM
Last modification on : Sunday, June 26, 2022 - 11:52:33 AM
Long-term archiving on: : Friday, October 26, 2012 - 3:20:27 PM


Files produced by the author(s)




Marc Daumas, Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. ACM Transactions on Mathematical Software, 2010, 37 (1), pp.1-20. ⟨10.1145/1644001.1644002⟩. ⟨hal-00127769v3⟩



Record views


Files downloads