Verifying OpenJDK's Sort Method for Generic Collections

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

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

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.
Original languageEnglish
Pages (from-to)93-126
Number of pages34
JournalJournal of Automated Reasoning
Volume62
Issue number1
DOIs
Publication statusPublished - Jan 2019

Fingerprint

Sorting
Merging

Cite this

Gouw, S. D., Boer, F. S. D., Bubel, R., Hähnle, R., Rot, J., & Steinhöfel, D. (2019). Verifying OpenJDK's Sort Method for Generic Collections. Journal of Automated Reasoning, 62(1), 93-126. https://doi.org/10.1007/s10817-017-9426-4
Gouw, Stijn de ; Boer, Frank S. de ; Bubel, Richard ; Hähnle, Reiner ; Rot, Jurriaan ; Steinhöfel, Dominic. / Verifying OpenJDK's Sort Method for Generic Collections. In: Journal of Automated Reasoning. 2019 ; Vol. 62, No. 1. pp. 93-126.
@article{9011c448e0dc4ffebf11f9caae936c1f,
title = "Verifying OpenJDK's Sort Method for Generic Collections",
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.",
author = "Gouw, {Stijn de} and Boer, {Frank S. de} and Richard Bubel and Reiner H{\"a}hnle and Jurriaan Rot and Dominic Steinh{\"o}fel",
year = "2019",
month = "1",
doi = "10.1007/s10817-017-9426-4",
language = "English",
volume = "62",
pages = "93--126",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "1",

}

Gouw, SD, Boer, FSD, Bubel, R, Hähnle, R, Rot, J & Steinhöfel, D 2019, 'Verifying OpenJDK's Sort Method for Generic Collections', Journal of Automated Reasoning, vol. 62, no. 1, pp. 93-126. https://doi.org/10.1007/s10817-017-9426-4

Verifying OpenJDK's Sort Method for Generic Collections. / Gouw, Stijn de; Boer, Frank S. de; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic.

In: Journal of Automated Reasoning, Vol. 62, No. 1, 01.2019, p. 93-126.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Verifying OpenJDK's Sort Method for Generic Collections

AU - Gouw, Stijn de

AU - Boer, Frank S. de

AU - Bubel, Richard

AU - Hähnle, Reiner

AU - Rot, Jurriaan

AU - Steinhöfel, Dominic

PY - 2019/1

Y1 - 2019/1

N2 - 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.

AB - 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.

U2 - 10.1007/s10817-017-9426-4

DO - 10.1007/s10817-017-9426-4

M3 - Article

VL - 62

SP - 93

EP - 126

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 1

ER -