A gallery of certified programs

This page collects several programs verified using Why.

Knuth's algorithm for prime number based on Bertrand's postulate: available here (code and proof by Laurent Théry)
A proof of GMP square root: available here (code and proof by Nicolas Magaud)

Note : Most Coq proofs require Coq 7.4.

Dijkstra's Dutch national flag
- Source: flag.mlw
- Coq proof: flag_why.v / Index
Levenshtein distance (code by Claude Marché)
- Source: distance.mlw
- Coq proof: words.v / distance_why.v / Index
Bresenham line drawing algorithm (proof of optimality)
- Source: bresenham.mlw
- Coq proof: zaux.v / bresenham_why.v / Index
Binary search
- Source: bsearch.mlw
- Coq proof: bsearch_why.v / Index
Integer square root (code and proof by Claude Marché)
- Source: sqrt.mlw
- Coq proof: sqrt_why.v / Index
Mac Carthy's 91 function
- Source: mac_carthy.mlw
- Coq proof: mac_carthy_why.v / Index
Knuth-Morris-Pratt string searching algorithm
- Source: kmp.mlw
- Coq proof: Lex.v / Match.v / Next.v / kmp_why.v / Index
Find, from this article: C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39-45, Jan 1971.
- Source: find.mlw
- Coq proof: find_spec.v / find_lemmas.v / find_proofs.v / find_why.v / Index
- The Coq proof is detailed in this paper

Maximum sort (code and proof by Sylvain Boulmé)
- Source: maximumsort.mlw
- Coq proof: maximumsort_why.v / Index
Selection sort
- Source: selection.mlw
- Coq proof: selection_why.v / Index
Quicksort
- Source: partition.mlw / quicksort.mlw
- Coq proof: Partition.v / Quicksort.v / partition_why.v / quicksort_why.v / Index
- The proof is detailed in this paper
Quicksort : a variant with a simpler partitioning, from Bentley's Programming Pearls
- Source: quicksort2.mlw
- Coq proof: quicksort2_why.v / Index
Heapsort (in place)
- Source: swap.mlw / downheap.mlw / heapsort.mlw
- Coq proof: heap.v / Inftree.v / swap_why.v / downheap_why.v / heapsort_why.v / Index
- The proof is detailed in this paper