Computer Science – Mathematical Software
Scientific paper
2007-01-29
Computer Science
Mathematical Software
Scientific paper
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.
Daumas Marc
Melquiond Guillaume
No associations
LandOfFree
Certification of bounds on expressions involving rounded operators does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Certification of bounds on expressions involving rounded operators, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Certification of bounds on expressions involving rounded operators will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-534141