Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
. 2019;62(1):93-126.
doi: 10.1007/s10817-017-9426-4. Epub 2017 Aug 31.

Verifying OpenJDK's Sort Method for Generic Collections

Stijn de Gouw  1 , Frank S de Boer  2   3 , Richard Bubel  4 , Reiner Hähnle  4 , Jurriaan Rot  5 , Dominic Steinhöfel  4
Affiliations

Verifying OpenJDK's Sort Method for Generic Collections

Stijn de Gouw et al. J Autom Reason. 2019.

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.

Keywords: Case study; Program verification; Specification; Theorem proving.

PubMed Disclaimer

Figures

Fig. 1
Fig. 1
Call dependencies of TimSort methods (excluding methods: minRunLength, rangeCheck and invocation of Java library methods like System.arraycopy)
Fig. 2
Fig. 2
Comparison of proof sizes with and without state merging. Only proofs where state merging has been applied are considered
Fig. 3
Fig. 3
Proportions of interactive rule applications (grouped by type) for all TimSort methods and excluding mergeLo
Fig. 4
Fig. 4
Number of interactive rules in mergeHi/mergeLo (grouped by type)
Fig. 5
Fig. 5
Distribution of interactive rules in mergeHi/mergeLo (grouped by type)
Fig. 6
Fig. 6
Schema of KeY ’s do-while transformation rule
Fig. 7
Fig. 7
New and improved do-while transformation (simplified)
See this image and copyright information in PMC

References

    1. Ahrendt W, Beckert B, Bubel R, Hähnle R, Schmitt P, Ulbrich M, editors. Deductive Software Verification—The KeY Book: From Theory to Practice, LNCS. Berlin: Springer; 2016.
    1. Ahrendt, W., Mostowski, W., Paganelli, G.: Real-time Java API specifications for high coverage test generation. In: Proceedings of the 10th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES ’12, pp. 145–154. ACM, New York (2012)
    1. Akbarpour B, Abdel-Hamid AT, Tahar S, Harrison J. Verifying a synthesized implementation of IEEE-754 floating-point exponential function using HOL. Comput. J. 2010;53(4):465–488. doi: 10.1093/comjnl/bxp023. - DOI
    1. Beckert B, Hähnle R. Reasoning and verification. IEEE Intell. Syst. 2014;29(1):20–29. doi: 10.1109/MIS.2014.3. - DOI
    1. Beckert B, Klebanov V. Proof reuse for deductive program verification. In: Cuellar J, Liu Z, editors. Proceedings, Software Engineering and Formal Methods (SEFM) Beijing: IEEE Press; 2004.

LinkOut - more resources