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/xx5hf6693cii51j32xibi4hv8zbgqg9x-coq-gappa-1.3.4.drv | ||
mips64el-linux | /gnu/store/frfy49i17m8hzpfvf9dmwdhgzlxxxfqh-coq-gappa-1.3.4.drv | ||
i686-linux | /gnu/store/xkm6bgkm9vxads0mqpkpbqrdsn18gxbj-coq-gappa-1.3.4.drv | ||
armhf-linux | /gnu/store/kczhwpyyc8hdi0qf6n9dbzab4fid5wn1-coq-gappa-1.3.4.drv | ||
aarch64-linux | /gnu/store/8hxc2pqb6rj4qcbpn5ng6c7cn7fivsj2-coq-gappa-1.3.4.drv |
Linter | Message | Location |
---|---|---|
formatting Look for formatting issues in the source | line 240 is way too long (94 characters) |