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

Sorting

Cite this

Gouw, Stijn de ; Boer, Frank S. de ; Rot, Jurriaan. / Proof Pearl : The KeY to Correct and Stable Sorting. In: Journal of Automated Reasoning. 2014 ; Vol. 53, No. 2. pp. 129-139.
@article{4b1d9fa6d98f40719c09048430d28554,
title = "Proof Pearl: The KeY to Correct and Stable Sorting",
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.",
author = "Gouw, {Stijn de} and Boer, {Frank S. de} and Jurriaan Rot",
year = "2014",
doi = "10.1007/s10817-013-9300-y",
language = "English",
volume = "53",
pages = "129--139",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "2",

}

Proof Pearl : The KeY to Correct and Stable Sorting. / Gouw, Stijn de; Boer, Frank S. de; Rot, Jurriaan.

In: Journal of Automated Reasoning, Vol. 53, No. 2, 2014, p. 129-139.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Proof Pearl

T2 - The KeY to Correct and Stable Sorting

AU - Gouw, Stijn de

AU - Boer, Frank S. de

AU - Rot, Jurriaan

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

U2 - 10.1007/s10817-013-9300-y

DO - 10.1007/s10817-013-9300-y

M3 - Article

VL - 53

SP - 129

EP - 139

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 2

ER -