Proof Pearl: The KeY to Correct and Stable Sorting

de Gouw, Stijn; de Boer, Frank; Rot, Jurriaan

doi:10.1007/s10817-013-9300-y

C.P.T. de Gouw (Stijn), F.S. de Boer (Frank) and J.C. Rot (Jurriaan)

2014-08-01

Proof Pearl: The KeY to Correct and Stable Sorting

Journal of Automated Reasoning , Volume 53 - Issue 2 p. 129- 139

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.

Additional Metadata
Keywords	Program Correctness, Mechanized Proof, Sorting, Counting Sort, Radix Sort, KeY
THEME	Software (theme 1)
Publisher	Springer
Persistent URL	doi.org/10.1007/s10817-013-9300-y
Journal	Journal of Automated Reasoning
Organisation	Computer Security
Citation APA Style AAA Style APA Style Cell Style Chicago Style Harvard Style IEEE Style MLA Style Nature Style Vancouver Style American-Institute-of-Physics Style Council-of-Science-Editors Style BibTex Format Endnote Format RIS Format CSL Format DOIs only Format	de Gouw, S., de Boer, F., & Rot, J. (2014). Proof Pearl: The KeY to Correct and Stable Sorting. Journal of Automated Reasoning, 53(2), 129–139. doi:10.1007/s10817-013-9300-y

View at Publisher

Free Full Text ( Final Version , 299kb )

Additional Files
Fulltext Final Version
Publisher Version

Proof Pearl: The KeY to Correct and Stable Sorting

Publication

Publication

Address

Publishing at CWI

Questions or comments?

Proof Pearl: The KeY to Correct and Stable Sorting

Publication

Publication

Workflow

Workflow

Add Content