We discuss a proof of the correctness of two sorting algorithms: Counting sort and Radix sort. The semi-automated proof is formalized in the state-of-the-art theorem prover KeY.
Program Correctness, Mechanized Proof, Sorting, Counting Sort, Radix Sort, KeY
Software (theme 1)
Springer
doi.org/10.1007/s10817-013-9300-y
Journal of Automated Reasoning
Computer Security

de Gouw, C.P.T, de Boer, F.S, & Rot, J.C. (2014). Proof Pearl: The KeY to Correct and Stable Sorting. Journal of Automated Reasoning, 53(2), 129–139. doi:10.1007/s10817-013-9300-y