Gappa 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 Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Certification of bounds on expressions involving rounded operators. Zbl 1364.68328Daumas, Marc; Melquiond, Guillaume 2010 all top 5 Cited by 34 Authors 6 Melquiond, Guillaume 5 Boldo, Sylvie 3 Filliâtre, Jean-Christophe 3 Muñoz, César A. 2 Clément, François 2 Dutle, Aaron 2 Konečný, Michal 2 Lauter, Christoph Quirin 2 Mayero, Micaela 2 Narkawicz, Anthony Joseph 2 Rümmer, Philipp 2 Weis, Pierre 2 Wintersteiger, Christoph M. 2 Zeljić, Aleksandar 1 Backeman, Peter 1 Bobot, François 1 Collins, Peter J. 1 Dartyge, Cécile 1 Daumas, Marc 1 de Dinechin, Florent 1 Duracz, Jan 1 Kumar, Ramana 1 Kupriianova, Olga 1 Marché, Claude 1 Mosaki, Elie 1 Moscato, Mariano M. 1 Muller, Jean-Michel 1 Niqui, Milad 1 Park, Sewon 1 Revol, Nathalie 1 Sárközy, András 1 Thies, Holger 1 Titolo, Laura 1 Weber, Tjark all top 5 Cited in 8 Serials 4 Journal of Automated Reasoning 2 Mathematics in Computer Science 1 Computers & Mathematics with Applications 1 ACM Transactions on Mathematical Software 1 IEEE Transactions on Computers 1 Formal Aspects of Computing 1 Annals of Mathematics and Artificial Intelligence 1 The Ramanujan Journal all top 5 Cited in 8 Fields 14 Computer science (68-XX) 13 Numerical analysis (65-XX) 2 Mathematical logic and foundations (03-XX) 2 Partial differential equations (35-XX) 1 Combinatorics (05-XX) 1 Number theory (11-XX) 1 Real functions (26-XX) 1 Special functions (33-XX) Citations by Year