Verifying OpenJDK's sort method for generic collections

DOI10.1007/S10817-017-9426-4MaRDI QIDQ1725846zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Frank S. de Boer, Richard Bubel, Reiner Hähnle, Jurriaan Rot, Dominic Steinhöfel, Stijn De Gouw

Publication date 15 February 2019

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

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10817-017-9426-4

zbMATH Keywords

specificationtheorem provingprogram verificationcase study

Mathematics Subject Classification ID

Searching and sorting (68P10) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Proving JDK's dual pivot quicksort correct
• An assertional proof of the stability and correctness of Natural Mergesort
• Verification of Java Programs with Generics
• On the worst-case complexity of TimSort
• A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms

Cites work

• scientific article; zbMATH DE number 437573 (Why is no real title available?)
• Fundamental Approaches to Software Engineering
• Hammering towards QED
• Isabelle. A generic theorem prover
• Proof of a recursive program: Quicksort
• Proof pearl: A mechanized proof of GHC's mergesort
• Proof pearl: The KeY to correct and stable sorting

Cited in

(7)

• An assertional proof of the stability and correctness of Natural Mergesort
• Proving JDK's dual pivot quicksort correct
• Fifty years of Hoare's logic
• Minimal coverability tree construction made complete and efficient
• A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms
• On the worst-case complexity of TimSort
• scientific article; zbMATH DE number 7378733 (Why is no real title available?)

Describes a project that uses

Uses Software

• AutoProof
• Quicksort
• KeY
• Isabelle
• Coq

This page was built for publication: Verifying OpenJDK's sort method for generic collections

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1725846)