Gappa
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 16 articles , 1 standard article )
Showing results 1 to 16 of 16.
Sorted by year (- Boldo, Sylvie; Melquiond, Guillaume: Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system (2017)
- Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
- 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)
- Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Trusting computations: a mechanized proof from partial differential equations to actual program (2014)
- 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; Marché, Claude: Formal verification of numerical programs: from C annotated programs to mechanical proofs (2011)
- Collins, Pieter; Niqui, Milad; Revol, Nathalie: A validated real function calculus (2011)
- de Dinechin, Florent; Lauter, Christoph; Melquiond, Guillaume: Certifying the floating-point implementation of an elementary function using Gappa (2011)
- Kumar, Ramana; Weber, Tjark: Validating QBF validity in HOL4 (2011)
- 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)