Verifying OpenJDK's sort method for generic collections

DOI10.1007/s10817-017-9426-4zbMath1468.68125OpenAlexW2751853904WikidataQ59527937 ScholiaQ59527937MaRDI QIDQ1725846

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

Publication date: 15 February 2019

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

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

zbMATH Keywords

theorem provingcase studyspecificationprogram verification

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)

Related Items

Minimal coverability tree construction made complete and efficient, Unnamed Item, Unnamed Item, Fifty years of Hoare's logic

Uses Software

• Coq
• Isabelle
• KeY
• Quicksort
• AutoProof

Cites Work

• Unnamed Item
• Isabelle. A generic theorem prover
• Proof pearl: A mechanized proof of GHC's mergesort
• Proof pearl: The KeY to correct and stable sorting
• Hammering towards QED
• Fundamental Approaches to Software Engineering
• Proof of a recursive program: Quicksort