Proof Pearl: The KeY to Correct and Stable Sorting

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

doi:10.1007/s10817-013-9300-y

Proof Pearl: The KeY to Correct and Stable Sorting

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

Research output: Contribution to journal › Article › Academic › peer-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 language	English
Pages (from-to)	129-139
Number of pages	11
Journal	Journal of Automated Reasoning
Volume	53
Issue number	2
DOIs	https://doi.org/10.1007/s10817-013-9300-y
Publication status	Published - 2014
Externally published	Yes

Fingerprint

Cite this

Gouw, S. D., Boer, F. S. D., & Rot, J. (2014). Proof Pearl: The KeY to Correct and Stable Sorting. Journal of Automated Reasoning, 53(2), 129-139. https://doi.org/10.1007/s10817-013-9300-y

@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",

}

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 -

Access to Document

10.1007/s10817-013-9300-y