d4a23d1cdb
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
6 lines
454 B
Text
6 lines
454 B
Text
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
|