Verifying OpenJDK's Sort Method for Generic Collections
The work
| Authors | Stijn de Gouw; Frank S. de Boer; Richard Bubel; Reiner Hähnle; Jurriaan Rot; Dominic Steinhöfel |
|---|---|
| Editors | |
| Type | article |
| Year | 2019 |
| Citekey | gouw2019verifying |
Where it appeared
| Published in | Journal of Automated Reasoning |
|---|---|
| Publisher | Springer |
| Volume | 62 |
| Issue | 1 |
| Pages | 93--126 |
Identifiers
| DOI | 10.1007/s10817-017-9426-4 |
|---|---|
| OpenAlex | W2751853904 |
Access
| Landing page | https://doi.org/10.1007/s10817-017-9426-4 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007/s10817-017-9426-4.pdf |
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.
Cite it as
@article{gouw2019verifying,
title = {Verifying OpenJDK's Sort Method for Generic Collections},
author = {Stijn de Gouw and Frank S. de Boer and Richard Bubel and Reiner Hähnle and Jurriaan Rot and Dominic Steinhöfel},
year = {2019},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = {62},
number = {1},
pages = {93--126},
doi = {10.1007/s10817-017-9426-4},
}
This record lives at https://refs.drheap.org/gouw2019verifying/ and will keep doing so.