./wip/gappa, Formal tool for certifying numerical applications

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 0.12.3, Package name: gappa-0.12.3, Maintainer: jihbed.research

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


Required to run:
[textproc/libxslt] [math/mpfr] [devel/gmp]

Required to build:
[devel/boost-headers] [pkgtools/cwrappers]

Master sites:

RMD160: b79deb8fe57d368099bcc27044fc31f3103b2f6e
Filesize: 244.324 KB

Version history: (Expand)

CVS history: (Expand)


   2012-09-29 02:50:33 by Aleksej Saushev | Files touched by this commit (158) 
Log message:
Drop superfluous PKG_DESTDIR_SUPPORT, "user-destdir" is default these days.
Mark packages that don't or might probably not have staged installation.
   2010-01-03 23:19:30 by Kamel Derouiche | Files touched by this commit (4) | Imported package
Log message:
Import gappa-0.12.3 as wip/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