OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case
The work
| Authors | Stijn de Gouw; Jurriaan Rot; Frank S. de Boer; Richard Bubel; Reiner Hähnle |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2015 |
| Citekey | gouw2015openjdks |
Where it appeared
| Published in | Computer Aided Verification |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 9206 |
| Pages | 273--289 |
Identifiers
| DOI | 10.1007/978-3-319-21690-4_16 |
|---|---|
| OpenAlex | W1002779697 |
Access
| Landing page | https://doi.org/10.1007/978-3-319-21690-4_16 |
|---|
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 perfor- mance. 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.
Cite it as
@inproceedings{gouw2015openjdks,
title = {OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case},
author = {Stijn de Gouw and Jurriaan Rot and Frank S. de Boer and Richard Bubel and Reiner Hähnle},
year = {2015},
booktitle = {Computer Aided Verification},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {273--289},
doi = {10.1007/978-3-319-21690-4_16},
}
This record lives at https://refs.drheap.org/gouw2015openjdks/ and will keep doing so.