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.
Type de document :
Article dans une revue
ACM Transactions on Mathematical Software, Association for Computing Machinery, 2010, 37 (1), pp.1-20. 〈10.1145/1644001.1644002〉
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

Contributeur : Guillaume Melquiond <>
Soumis le : mardi 9 novembre 2010 - 13:43:22
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:20:27


Fichiers produits par l'(les) auteur(s)




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



Consultations de la notice


Téléchargements de fichiers