The ProVal team was stopped at the end of August 2012, and reborn into a new team
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.
Examples involving a predicate defined inductively
- Selection Sort, C version
- Fibonacci sequence, linear algorithm, Java version
- Edition distance
- Program verification examples from the book "Software Foundations"
- Tree relabelling
- In-Place Linked-List Reversal in Why3