@Article{Daumas:2009:CBE,
  author =       "Marc Daumas and Guillaume Melquiond",
  title =        "Certification of Bounds on Expressions Involving Rounded
                  Operators",
  journal =      "{ACM} Transactions on Mathematical Software",
  volume =       "37",
  number =       "1",
  accepted =     "2 February 2009",
  upcoming =     "true", 
  abstract =     "
                 Gappa uses interval arithmetic to certify bounds on
                 mathematical expressions that involve rounded as well
                 as exact operators. It 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
                 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 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.",
}