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.
, , , , ,
Journal of Automated Reasoning
Computer Security

de Gouw, S., de Boer, F., & Rot, J. (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