Proof Pearl: The KeY to Correct and Stable Sorting

Stijn de Gouw, Frank S. de Boer, Jurriaan Rot

Research output: Contribution to journalArticleAcademicpeer-review


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.
Original languageEnglish
Pages (from-to)129-139
Number of pages11
JournalJournal of Automated Reasoning
Issue number2
Publication statusPublished - 2014
Externally publishedYes


Dive into the research topics of 'Proof Pearl: The KeY to Correct and Stable Sorting'. Together they form a unique fingerprint.

Cite this