Proof generator for arithmetic properties
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 Why3 software verification platform or as an automatic tactic for the Coq proof assistant.
| System | Target | Derivation | Build status |
|---|---|---|---|
| x86_64-linux | /gnu/store/ii5086nxyhqf43qwr2il1yy1k9gm5aqf-gappa-1.3.5.drv | ||
| x86_64-linux | i586-pc-gnu | /gnu/store/bisixzcbmqnsaslnn2va82hxacpd1gib-gappa-1.3.5.drv | |
| x86_64-linux | arm-linux-gnueabihf | /gnu/store/4ywllkj2g1s2pf2jbfbn36axvmm6h9pj-gappa-1.3.5.drv | |
| x86_64-linux | aarch64-linux-gnu | /gnu/store/5kmq6mjihw91b1l487qpi1s58rpn4p5m-gappa-1.3.5.drv | |
| riscv64-linux | /gnu/store/zd5n19nk4d7dxiw1lmbrqwxswl0paqc7-gappa-1.3.5.drv | ||
| powerpc-linux | /gnu/store/wg35ic35xnj7vq1b5mjqmp0zsn45f3fv-gappa-1.3.5.drv | ||
| powerpc64le-linux | /gnu/store/ym3whryfij2504lzjzw68j7i610r79l1-gappa-1.3.5.drv | ||
| mips64el-linux | /gnu/store/rb4bidh8kflqgbcm5gzlb8y5ghxhlqk1-gappa-1.3.5.drv | ||
| i686-linux | /gnu/store/l0lp529a41225hh7xxddhdrhp06idg2r-gappa-1.3.5.drv | ||
| i586-gnu | /gnu/store/vpdg4jqpr77immsykvz6nzjm35m6g12v-gappa-1.3.5.drv | ||
| armhf-linux | /gnu/store/s26f0jsq78md7vsgci4pllqxzmqyjv39-gappa-1.3.5.drv | ||
| aarch64-linux | /gnu/store/gjy533x7rkf6vdwafbsg9giy5ymdmk11-gappa-1.3.5.drv |
| Linter | Message | Location |
|---|---|---|
| optional-tests Make sure tests are only run when requested | the 'check' phase should respect #:tests? |