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

  • Abstract depth first search (white initial color) (proof1, proof2, coq)

  • nwtb invariant for DFS in undirected graph (proof)

  • Random search walk (proof1, proof2)

  • Abstract depth first search (proof1, proof2, proof1b, proof2b, coq)

  • Breadth first search (proof)

  • Iterative depth first search with stack (proof)

  • GraphSet module (proof)

  • Depth first search (array + list) (proof)

  • Depth first search as in Sedgewick (proof)

  • Strongly connected components - Tarjan 1972 (abs) (proof1, proof2, proof3)

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

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

  • Acyclicity test (abs) (proof)




     
    Jean-Jacques Lévy
    Chen Ran

    
    

  • Generated by why3doc 0.83