Proof Pearl: The KeY to Correct and Stable Sorting

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

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

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
Volume53
Issue number2
DOIs
Publication statusPublished - 2014
Externally publishedYes

    Fingerprint

Cite this