The ProVal team was stopped at the end of August 2012, and reborn into a new team
Toccata

These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

## Non-linear Arithmetic

Examples involving reasoning in non-linear arithmetic

- Sum of multiples of 3 and 5
- Floating-point square root using Newton iteration
- Approximated Cosine in C annotated in ACSL
- Approximated Cosine in Why3
- Fast exponentiation
- Integer square root
- Bresenham line drawing algorithm
- Binary Square Root