# Sorting algorithms

• Selection sort (proof1, proof2)

• Bubble sort (proof1, proof2)

• Insertion sort (proof1, proof2; proof3). Stability (proof4)

• Insertion sort in lists (proof1, proof2)

• Insertion in sorted trees (proof1, proof2).

• Quicksort (proof, coq1, coq2)

• Mergesort on lists (proof1, proof2)

• Mergesort (proof1, proof2; coq1, coq2 )

# Graph algorithms

• GraphSet module (proof)

• Abstract depth first search (white initial color) (proof1, proof2; proof3, proof4)

• The white-path theorem for depth first search (proof == sound + complete)

• The white-path theorem for depth first search [with black and gray sets] (proof == sound + complete)

• Abstract DFS: no white to black edge for undirected graph (proof)

• Random search walk (sound + complete; sound2)

• Breadth first search (sound, complete)

• Iterative depth first search with a stack (sound, complete)

• Depth first search (mutable visited set) (sound, complete)

• Depth first search (list of vertices + mutable visited set) (sound, complete)

• Depth first search (list of vertices + mutable visited set + color) (sound, complete)

• Depth first search as in Sedgewick (sound, complete; with graph array sound; complete)

• Strongly connected components - Tarjan 1972 (with ranks and explicit grays) (proof1)

• SCC - Tarjan 1972 (with just ranks) (weak, strong)

• SCC - Tarjan 1972 (with precedes) (weak, strong) [ a ]

• Strongly connected components - Tarjan 1972 (quasi imperative) (proof)

• Strongly connected components - Kosaraju 1978 (abs) (proof)

• Articulation points (weak, strong)

• Biconnected components (weak, strong)

• Acyclicity test (functional, imperative)

• Generated by why3doc 0.83