TU Darmstadt / ULB / TUbiblio

Verifying OpenJDK's Sort Method for Generic Collections

de Gouw, Stijn and de Boer, Frank S. and Bubel, Richard and Hähnle, Reiner and Rot, Jurriaan and Steinhöfel, Dominic (2017):
Verifying OpenJDK's Sort Method for Generic Collections.
In: Journal of Automated Reasoning, ISSN 1573-0670, DOI: 10.1007/s10817-017-9426-4, [Online-Edition: https://doi.org/10.1007/s10817-017-9426-4],
[Article]

Abstract

TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we discovered a bug which causes the implementation to crash by an uncaught exception. In this paper, we identify conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise performance. We formally specify the new version and verify termination and the absence of exceptions including the bug. This verification is carried out mechanically with KeY, a state-of-the-art interactive verification tool for Java. We provide a detailed description and analysis of the proofs. The complexity of the proofs required extensions and new capabilities in KeY, including symbolic state merging.

Item Type: Article
Erschienen: 2017
Creators: de Gouw, Stijn and de Boer, Frank S. and Bubel, Richard and Hähnle, Reiner and Rot, Jurriaan and Steinhöfel, Dominic
Title: Verifying OpenJDK's Sort Method for Generic Collections
Language: German
Abstract:

TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we discovered a bug which causes the implementation to crash by an uncaught exception. In this paper, we identify conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise performance. We formally specify the new version and verify termination and the absence of exceptions including the bug. This verification is carried out mechanically with KeY, a state-of-the-art interactive verification tool for Java. We provide a detailed description and analysis of the proofs. The complexity of the proofs required extensions and new capabilities in KeY, including symbolic state merging.

Journal or Publication Title: Journal of Automated Reasoning
Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Date Deposited: 16 May 2018 09:43
DOI: 10.1007/s10817-017-9426-4
Official URL: https://doi.org/10.1007/s10817-017-9426-4
Export:

Optionen (nur für Redakteure)

View Item View Item