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.

## Jessie

http://www.frama-c.com/jessie.html

Jessie is a deductive verification plug-in of Frama-C, using Why as back-end

- Veltkamp/Dekker algorithm
- Insertion Sort, C version
- Selection Sort, C version
- Binary search in C annotated in ACSL
- Scalar product of vectors using floating-point numbers
- Drift of a clock using floating-point numbers
- Approximated Cosine, exact values and rounding errors
- Approximated Cosine in C annotated in ACSL
- FoVeOOS'11 Competition: challenge 3, in C
- FoVeOOS'11 Competition: challenge 2, in C
- FoVeOOS'11 Competition: challenge 1, in C