swMATH ID: 4885
Software Authors: Guillaume Melquiond
Description: 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.
Homepage: http://gappa.gforge.inria.fr/
Keywords: software verification; automatical prove
Related Software: Coq; z3; ASTREE; PVS; Why3; Flocq; cvc3; ACSL; Caduceus; KRAKATOA; MetiTarski; Frama-C; dReal; HOL Light; RealPaver; ACL2; MathSAT5; Sollya; Haskell; iRRAM
Cited in: 19 Publications

Citations by Year