User’s Guide for Gappa

Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques — automatic proof generation of arithmetic properties) is a tool intended to help verifying and formally proving properties on numerical programs and circuits handling floating-point or fixed-point arithmetic.

This tool manipulates logical formulas stating the enclosures of expressions in some intervals. For example, a formal proof of the property

\[c \in [-0.3,-0.1] ~\land~ (2a \in [3,4] \Rightarrow b+c \in [1,2]) ~\land~ a-c \in [1.9,2.05] \quad \Rightarrow \quad b+1 \in [2,3.5]\]

can be generated thanks to the following Gappa script.

{ c in [-0.3,-0.1] /\
  (2 * a in [3,4] -> b + c in [1,2]) /\
  a - c in [1.9,2.05]

  -> b + 1 in [2,3.5] }

Through the use of rounding operators as part of the expressions, Gappa is specially designed to deal with formulas that could appear when certifying numerical codes. In particular, Gappa makes it simple to bound computational errors due to floating-point arithmetic.

Gappa is free software; you can redistribute it and/or modify it under the terms of the CeCILL Free Software License Agreement or under the terms of the GNU General Public License. (Refer to the files from the source archive for the precise wording of these two licenses.) Gappa can be downloaded on its project page. The tool and its documentation have been written by Guillaume Melquiond.