Certification of bounds on expressions involving rounded operators

TL;DR

Gappa is a tool that certifies bounds on mathematical expressions with rounded operators using interval arithmetic, generating verifiable proofs checked by Coq or HOL Light, and supports complex bounds and software correctness proofs.

Contribution

This paper introduces Gappa, a novel tool that combines interval arithmetic, proof generation, and verification for bounds involving rounded operators, enhancing formal certification capabilities.

Findings

Gappa can generate and verify proofs of bounds using Coq or HOL Light.

It handles complex bounds with interval properties and rewriting rules.

Gappa is effective for verifying small software correctness proofs.

Abstract

Gappa uses interval arithmetic to certify bounds on mathematical expressions that involve rounded as well as exact operators. Gappa generates a theorem with its proof for each bound treated. The proof can be checked with a higher order logic automatic proof checker, either Coq or HOL Light, and we have developed a large companion library of verified facts for Coq dealing with the addition, multiplication, division, and square root, in 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 is used to quickly obtain coarse bounds. It can also 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 perfectly suited to the proof of correctness of small pieces of software. Proof obligations can be written by designers, produced by third-party tools or obtained by overloading arithmetic operators.