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.

References in zbMATH (referenced in 13 articles , 1 standard article )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
  2. Muller, Jean-Michel: Elementary functions. Algorithms and implementation (2016)
  3. 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)
  4. Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
  5. Kupriianova, Olga; Lauter, Christoph: Metalibm: a mathematical functions code generator (2014)
  6. 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)
  7. Muñoz, César; Narkawicz, Anthony: Formalization of Bernstein polynomials and applications to global optimization (2013)
  8. Boldo, Sylvie; Marché, Claude: Formal verification of numerical programs: from C annotated programs to mechanical proofs (2011)
  9. Collins, Pieter; Niqui, Milad; Revol, Nathalie: A validated real function calculus (2011)
  10. de Dinechin, Florent; Lauter, Christoph; Melquiond, Guillaume: Certifying the floating-point implementation of an elementary function using Gappa (2011)
  11. Daumas, Marc; Melquiond, Guillaume: Certification of bounds on expressions involving rounded operators (2010)
  12. Boldo, Sylvie; Filli^atre, Jean-Christophe; Melquiond, Guillaume: Combining Coq and Gappa for certifying floating-point programs (2009)
  13. 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)