Verifying OpenJDK’s Sort Method for Generic Collections

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...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2019-01, Vol.62 (1), p.93-126
Main Authors: de Gouw, Stijn, de Boer, Frank S., Bubel, Richard, Hähnle, Reiner, Rot, Jurriaan, Steinhöfel, Dominic
Format: Article
Language:English
Subjects:
Artificial Intelligence
Classification
Computer Science
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Sorting algorithms
State of the art
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-017-9426-4