Certification of bounds on expressions involving rounded operators

Marc Daumas, Guillaume Melquiond

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 boun…