see also the index (by topic, by tool, by reference, by year)
Gappa
Tool for verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic
- Approximated Cosine in C annotated in ACSL
- Approximated Cosine in Why3
- Approximated Cosine, exact values and rounding errors
- Drift of a clock using floating-point numbers
- Floating-point square root using Newton iteration
- Iterated quaternion multiplication
- KB3D: an avionics example
- Scalar product of vectors using floating-point numbers
- Veltkamp/Dekker algorithm
see also the index (by topic, by tool, by reference, by year)