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 18 articles , 1 standard article )

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

  1. Dutle, Aaron; Moscato, Mariano; Titolo, Laura; Muñoz, César; Anderson, Gregory; Bobot, François: Formal analysis of the compact position reporting algorithm (2021)
  2. Zeljić, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp: Exploring approximations for floating-point arithmetic using uppsat (2018)
  3. Boldo, Sylvie; Melquiond, Guillaume: Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system (2017)
  4. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
  5. Muller, Jean-Michel: Elementary functions. Algorithms and implementation (2016)
  6. 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)
  7. Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Trusting computations: a mechanized proof from partial differential equations to actual program (2014)
  8. Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
  9. Kupriianova, Olga; Lauter, Christoph: Metalibm: a mathematical functions code generator (2014)
  10. Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)
  11. Muñoz, César; Narkawicz, Anthony: Formalization of Bernstein polynomials and applications to global optimization (2013)
  12. Boldo, Sylvie; Marché, Claude: Formal verification of numerical programs: from C annotated programs to mechanical proofs (2011)
  13. Collins, Pieter; Niqui, Milad; Revol, Nathalie: A validated real function calculus (2011)
  14. de Dinechin, Florent; Lauter, Christoph; Melquiond, Guillaume: Certifying the floating-point implementation of an elementary function using Gappa (2011)
  15. Kumar, Ramana; Weber, Tjark: Validating QBF validity in HOL4 (2011)
  16. Daumas, Marc; Melquiond, Guillaume: Certification of bounds on expressions involving rounded operators (2010)
  17. Boldo, Sylvie; Filliâtre, Jean-Christophe; Melquiond, Guillaume: Combining Coq and Gappa for certifying floating-point programs (2009)
  18. 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)