OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case
Presented at the International Conference on Computer Aided Verification, San Francisco, CA, USA
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.
|Software/Program Verification (acm D.2.4), Specifying and Verifying and Reasoning about Programs (acm F.3.1)|
|Software (theme 1)|
|D. Kroening , C.S. Pasareanu|
|Engineering Virtualized Services|
|International Conference on Computer Aided Verification|
|Published paper: DOI: 10.1007/978-3-319-21690-4_16|
de Gouw, C.P.T, Rot, J.C, de Boer, F.S, Bubel, R, & Haehnle, R. (2015). OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case. In D Kroening & C.S Pasareanu (Eds.), .