Proof Pearl: The KeY to Correct and Stable Sorting

The work

AuthorsStijn de Gouw; Frank S. de Boer; Jurriaan Rot
Editors
Typearticle
Year2014
Citekeygouw2014proof

Where it appeared

Published inJournal of Automated Reasoning
PublisherSpringer
Volume53
Issue2
Pages129--139

Identifiers

DOI10.1007/s10817-013-9300-y
OpenAlexW1998392058

Access

Landing pagehttps://doi.org/10.1007/s10817-013-9300-y
Free full texthttps://ir.cwi.nl/pub/23074

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.

A copy is held

pdf, 299.3 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-16 15:23 UTC

Filed under

deboer degouw jar rot verifying-real-java

Cite it as

@article{gouw2014proof,
  title        = {Proof Pearl: The KeY to Correct and Stable Sorting},
  author       = {Stijn de Gouw and Frank S. de Boer and Jurriaan Rot},
  year         = {2014},
  journal      = {Journal of Automated Reasoning},
  publisher    = {Springer},
  volume       = {53},
  number       = {2},
  pages        = {129--139},
  doi          = {10.1007/s10817-013-9300-y},
}

This record lives at https://refs.drheap.org/gouw2014proof/ and will keep doing so.