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 Dive into the research topics of 'OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case'. Together they form a unique fingerprint.

  • 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