OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case

Stijn de Gouw, Jurriaan Rot, Frank S. de Boer, Richard Bubel, Reiner Hähnle

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

Abstract

We investigate the correctness of TimSort, which is the main sorting algorithm provided by the Java standard library. The goal is functional verification with mechanical proofs. During our verification attempt we discovered a bug which causes the implementation to crash. We characterize the conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise the performance. We formally specify the new version and mechanically verify the absence of this bug with KeY, a state-of-the-art verification tool for Java.
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I
EditorsDaniel Kroening , Corina S. Păsăreanu
PublisherSpringer
Pages273-289
Number of pages17
ISBN (Electronic)978-3-319-21690-4
ISBN (Print)978-3-319-21689-8
DOIs
Publication statusPublished - 2015
Event27th International Conference on Computer Aided Verification - San Francisco, United States
Duration: 18 Jul 201524 Jul 2015
http://i-cav.org/2015/

Conference

Conference27th International Conference on Computer Aided Verification
Abbreviated titleCAV 2015
CountryUnited States
CitySan Francisco
Period18/07/1524/07/15
Internet address

Fingerprint

Sorting

Cite this

Gouw, S. D., Rot, J., Boer, F. S. D., Bubel, R., & Hähnle, R. (2015). OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case. In D. K., & C. S. Păsăreanu (Eds.), Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I (pp. 273-289). Springer. https://doi.org/10.1007/978-3-319-21690-4_16
Gouw, Stijn de ; Rot, Jurriaan ; Boer, Frank S. de ; Bubel, Richard ; Hähnle, Reiner. / OpenJDK's Java.utils.Collection.sort() Is Broken : The Good, the Bad and the Worst Case. Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. editor / Daniel Kroening ; Corina S. Păsăreanu. Springer, 2015. pp. 273-289
@inproceedings{63f9bada1b3c40d1ba5dc3ca2687a9c7,
title = "OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case",
abstract = "We investigate the correctness of TimSort, which is the main sorting algorithm provided by the Java standard library. The goal is functional verification with mechanical proofs. During our verification attempt we discovered a bug which causes the implementation to crash. We characterize the conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise the performance. We formally specify the new version and mechanically verify the absence of this bug with KeY, a state-of-the-art verification tool for Java.",
author = "Gouw, {Stijn de} and Jurriaan Rot and Boer, {Frank S. de} and Richard Bubel and Reiner H{\"a}hnle",
year = "2015",
doi = "10.1007/978-3-319-21690-4_16",
language = "English",
isbn = "978-3-319-21689-8",
pages = "273--289",
editor = "{Daniel Kroening} and Păsăreanu, {Corina S.}",
booktitle = "Computer Aided Verification",
publisher = "Springer",

}

Gouw, SD, Rot, J, Boer, FSD, Bubel, R & Hähnle, R 2015, OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case. in DK & CS Păsăreanu (eds), Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Springer, pp. 273-289, 27th International Conference on Computer Aided Verification, San Francisco, United States, 18/07/15. https://doi.org/10.1007/978-3-319-21690-4_16

OpenJDK's Java.utils.Collection.sort() Is Broken : The Good, the Bad and the Worst Case. / Gouw, Stijn de; Rot, Jurriaan; Boer, Frank S. de; Bubel, Richard; Hähnle, Reiner.

Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. ed. / Daniel Kroening; Corina S. Păsăreanu. Springer, 2015. p. 273-289.

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

TY - GEN

T1 - OpenJDK's Java.utils.Collection.sort() Is Broken

T2 - The Good, the Bad and the Worst Case

AU - Gouw, Stijn de

AU - Rot, Jurriaan

AU - Boer, Frank S. de

AU - Bubel, Richard

AU - Hähnle, Reiner

PY - 2015

Y1 - 2015

N2 - We investigate the correctness of TimSort, which is the main sorting algorithm provided by the Java standard library. The goal is functional verification with mechanical proofs. During our verification attempt we discovered a bug which causes the implementation to crash. We characterize the conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise the performance. We formally specify the new version and mechanically verify the absence of this bug with KeY, a state-of-the-art verification tool for Java.

AB - We investigate the correctness of TimSort, which is the main sorting algorithm provided by the Java standard library. The goal is functional verification with mechanical proofs. During our verification attempt we discovered a bug which causes the implementation to crash. We characterize the conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise the performance. We formally specify the new version and mechanically verify the absence of this bug with KeY, a state-of-the-art verification tool for Java.

UR - https://link.springer.com/book/10.1007/978-3-319-21690-4

U2 - 10.1007/978-3-319-21690-4_16

DO - 10.1007/978-3-319-21690-4_16

M3 - Conference article in proceeding

SN - 978-3-319-21689-8

SP - 273

EP - 289

BT - Computer Aided Verification

A2 - , Daniel Kroening

A2 - Păsăreanu, Corina S.

PB - Springer

ER -

Gouw SD, Rot J, Boer FSD, Bubel R, Hähnle R. OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case. In DK, Păsăreanu CS, editors, Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Springer. 2015. p. 273-289 https://doi.org/10.1007/978-3-319-21690-4_16