OpenJDK's Java']Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case

被引：42

作者：

de Gouw, Stijn ^{[1
,2
]}

Rot, Jurriaan ^{[1
,3
]}

de Boer, Frank S. ^{[1
,3
]}

Bubel, Richard ^{[4
]}

Haehnle, Reiner ^{[4
]}

机构：

[1] CWI, NL-1009 AB Amsterdam, Netherlands

[2] SDL, Amsterdam, Netherlands

[3] Leiden Univ, Leiden, Netherlands

[4] Tech Univ Darmstadt, Darmstadt, Germany

来源：

COMPUTER AIDED VERIFICATION, PT I | 2015年 / 9206卷

关键词：

VERIFICATION; PROOF;

D O I：

10.1007/978-3-319-21690-4_16

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：273 / 289

页数：17

共 16 条

[1]

Ahrendt W, 2012, PROCEEDINGS OF THE 10TH INTERNATIONAL WORKSHOP ON JAVA TECHNOLOGIES FOR REAL-TIME AND EMBEDDED SYSTEMS, P145

[2] Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL [J].

Akbarpour, Behzad ;

Abdel-Hamid, Amr T. ;

Tahar, Sofiene ;

Harrison, John .

COMPUTER JOURNAL, 2010, 53 (04) :465-488

[3] Reasoning and Verification: State of the Art and Current Trends [J].

Beckert, Bernhard ;

Haehnle, Reiner .

IEEE INTELLIGENT SYSTEMS, 2014, 29 (01) :20-29

[4]

Beckert Bernhard., 2007, LNCS, V4334

[5]

Bubel R, 2014, LECT NOTES COMPUT SC, V8803, P120, DOI 10.1007/978-3-662-45231-8_9

[6]

de Gouw S., WEB APPENDIX THIS PA

[7] Proof Pearl: The KeY to Correct and Stable Sorting [J].

de Gouw, Stijn ;

de Boer, Frank ;

Rot, Jurriaan .

JOURNAL OF AUTOMATED REASONING, 2014, 53 (02) :129-139

[8]

Filliatre J. C., 1999, THEOREM PROVING HIGH

[9] PROOF OF A RECURSIVE PROGRAM - QUICKSORT [J].

FOLEY, M ;

HOARE, CAR .

COMPUTER JOURNAL, 1971, 14 (04) :391-&

[10]

Hahnle Reiner, 2013, Automated Deduction - CADE-24. 24th International Conference on Automated Deduction. Proceedings: LNCS 7898, P300, DOI 10.1007/978-3-642-38574-2_21

← 1 2 →