L'équipe ProVal s'est arrêtée à la fin août 2012, et renaît en une nouvelle équipe
Toccata
Ces pages n'évoluent plus, suivez le lien ci-dessus pour les informations à
jour sur notre équipe.
Jean-Christophe Filliâtre
- Binary search in C annotated in ACSL
- Red-black trees
- Unraveling a Card Trick
- Snapshotable Trees
- Boyer and Moore's MJRTY algorithm (1980)
- Hash table implementation
- Generate all binary trees of size n
- Find the maximal element in an array
- Dijkstra's national flag (variant)
- An example from EWD 673
- Sort an array of integers, assuming all elements are in the range 0..k-1
- Bellman-Ford algorithm
- Traversing a tree inorder, filling an array
- Maximal sum in a matrix
- Computing the number of solutions to the N-queens puzzle
- Find a value in a sorted list of integers
- Knuth's prime numbers
- Knuth-Morris-Pratt string searching algorithm
- FoVeOOS'11 Competition: challenge 3 in Why3
- FoVeOOS'11 Competition: challenge 2 in Why3
- Hoare's Proof of a Program: FIND
- Tortoise and hare algorithm
- Proof from Turing's Checking a Large Routine (1949)
- Program proofs from Floyd's Assigning Meanings to Programs (1967)
- Greatest common divisor with Bezout coefficients
- Greatest common divisor, using the Euclidean algorithm
- Searching a zero in an array where values never decrease by more than one
- Various programs computing the factorial, in Why3
- Fibonacci function, linear/logarithmic algorithms, Why3 version
- Fibonacci with memoization
- Extract non-zero values from an array
- Edition distance
- Dijkstra's national flag
- Program verification examples from the book "Software Foundations"
- Same fringe
- Tree relabelling
- Quicksort (arrays)
- Fast exponentiation
- Mergesort (lists)
- McCarthy's 91 function
- Selection sort (arrays)
- Insertion sort (arrays)
- Insertion sort (lists)
- Bresenham line drawing algorithm
- Binary search
- Algorithm 65 (find)
- Algorithm 64 (quicksort)
- Algorithm 63 (partition)
- Binary Square Root
- Optimal replay
- Resizable arrays
- The N-queens problem, in C with Caduceus tool
- Amortized Queue, in Why3
- The N-queens problem, in Why3
- Searching a Linked List, in Why3
- Inverting an Injection, in Why3
- Sum and Maximum, in Why3
- Find the shortest path in a directed graph using BFS
- Tree reconstruction from a list of leave depths
- Circular queue in an array
- Call-by-value reduction of SK terms
- Sort an array of Boolean values
- Sparse Arrays in Why3