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.
Additional Metadata
Keywords Program Correctness, Mechanized Proof, Sorting, Counting Sort, Radix Sort, KeY
THEME Software (theme 1)
Publisher Springer
Persistent URL dx.doi.org/10.1007/s10817-013-9300-y
Journal Journal of Automated Reasoning
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