Gappa is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act as a backend prover for the Why software verification plateform or as an automatic tactic for the Coq proof assistant.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Muller, Jean-Michel: Elementary functions. Algorithms and implementation (to appear) (2016)
- Narkawicz, Anthony; Muñoz, César; Dutle, Aaron: Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems (2015)
- Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
- Kupriianova, Olga; Lauter, Christoph: Metalibm: a mathematical functions code generator (2014)
- Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)
- Muñoz, César; Narkawicz, Anthony: Formalization of Bernstein polynomials and applications to global optimization (2013)
- Boldo, Sylvie; Filli^atre, Jean-Christophe; Melquiond, Guillaume: Combining Coq and Gappa for certifying floating-point programs (2009)
- Dartyge, Cécile; Mosaki, Elie; Sárközy, András: On large families of subsets of the set of the integers not exceeding $N$ (2009)