Proof pearl: The KeY to correct and stable sorting

DOI10.1007/s10817-013-9300-yzbMath1314.68277OpenAlexW1998392058MaRDI QIDQ2351413

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

Publication date: 23 June 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/23074

zbMATH Keywords

sortingcorrectnessradix sortcounting sorttheorem prover \texttt{KeY}

Mathematics Subject Classification ID

Searching and sorting (68P10)

Related Items (4)

An Assertional Proof of the Stability and Correctness of Natural Mergesort ⋮ Integrating ADTs in KeY and their application to history-based reasoning about collection ⋮ Minimal coverability tree construction made complete and efficient ⋮ Verifying OpenJDK's sort method for generic collections

Uses Software

• Coq
• JML
• KeY
• Quicksort

Cites Work

• Verification of object-oriented programs: a transformational approach
• Verification of sequential and concurrent programs
• Proof pearl: A mechanized proof of GHC's mergesort
• Information Flow in Object-Oriented Software
• Fundamental Approaches to Software Engineering
• KeY: A Formal Method for Object-Oriented Systems
• Proof of a recursive program: Quicksort

This page was built for publication: Proof pearl: The KeY to correct and stable sorting