Verify and formally prove properties on numerical programs
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 plateform or as an automatic tactic for the Coq proof assistant.
| System | Target | Derivation | Build status |
|---|---|---|---|
| x86_64-linux | /gnu/store/r2i7rga9pd9iyfhfl02cqkz5a00wwms6-coq-gappa-1.3.4.drv | ||
| mips64el-linux | /gnu/store/yi0kvwayywdai2h2d54vfw3flyfaab8i-coq-gappa-1.3.4.drv | ||
| i686-linux | /gnu/store/6cbi7dc1gadghr9r69x7ypima4pgk40d-coq-gappa-1.3.4.drv | ||
| armhf-linux | /gnu/store/z0iyr81s95nvvdaf5dpvv9zjw9afgzaf-coq-gappa-1.3.4.drv | ||
| aarch64-linux | /gnu/store/v3a8208g965rxc0s49z1v4hr1f7ygavc-coq-gappa-1.3.4.drv |
| Linter | Message | Location |
|---|---|---|
| formatting Look for formatting issues in the source | line 265 is way too long (94 characters) |