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 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Muller, Jean-Michel: Elementary functions. Algorithms and implementation (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)
- Daumas, Marc; Melquiond, Guillaume: Certification of bounds on expressions involving rounded operators (2010)
- 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)