Verification of counting sort and radix sort
Sorting is an important algorithmic task used in many applications. Two main aspects of sorting algorithms which have been studied extensively are complexity and correctness. [Foley and Hoare, 1971] published the first formal correctness proof of a sorting algorithm (Quicksort). While this is a handwritten proof, the development and application of (semi)-automated theorem provers has since taken a huge flight. The major sorting algorithms Insertion sort, Heapsort and Quicksort were proven correct by Filliâtre and Magaud  using the proof assistant Coq. Recently, Sternagel  formalized a proof of Mergesort within the interactive theorem prover Isabelle/HOL.
|Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence|
|Organisation||Centrum Wiskunde & Informatica, Amsterdam, The Netherlands|
de Gouw, C.P.T, de Boer, F.S, & Rot, J.C. (2016). Verification of counting sort and radix sort. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence. doi:10.1007/978-3-319-49812-6_19