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.
Tricky termination
Examples involving a tricky termination argument
- Binary search in C annotated in ACSL
- McCarthy 91 function, Java version
- Tortoise and hare algorithm
- Quicksort (arrays)
- McCarthy's 91 function
- Integer square root
- Binary search
- The N-queens problem, in C with Caduceus tool