Formally Verifying an Efficient Sorter

被引：1
作者：
Beckert, Bernhard [1 ]
Sanders, Peter [1 ]
Ulbrich, Mattias [1 ]
Wiesler, Julian [1 ]
Witt, Sascha [1 ]
机构：
[1] Karlsruhe Inst Technol, Karlsruhe, Germany
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2024 | 2024年 / 14570卷
关键词：
VERIFICATION;
D O I：
10.1007/978-3-031-57246-3_15
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
In this experience report, we present the complete formal verification of a Java implementation of inplace superscalar sample sort (ips(4)o) using the KeY program verification system. As ips(4)o is one of the fastest general purpose sorting algorithms, this is an important step towards a collection of basic toolbox components that are both provably correct and highly efficient. At the same time, it is an important case study of how careful, highly efficient implementations of complicated algorithms can be formally verified directly. We provide an analysis of which features of the KeY system and its verification calculus are instrumental in enabling algorithm verification without any compromise on algorithm efficiency.
引用
收藏
页码：268 / 287
页数：20
相关论文
共 37 条
  • [1] Ahrendt W, 2016, LECT NOTES COMPUT SC, V10001, P1, DOI 10.1007/978-3-319-49812-6
  • [2] Engineering In-place (Shared-memory) Sorting Algorithms
    Axtmann, Michael
    Witt, Sascha
    Ferizovic, Daniel
    Sanders, Peter
    [J]. ACM TRANSACTIONS ON PARALLEL COMPUTING, 2022, 9 (01)
  • [3] Beckert B., 2024, Tech. rep., DOI [10.5445/IR/1000167846, DOI 10.5445/IR/1000167846]
  • [4] Proving JDK's Dual Pivot Quicksort Correct
    Beckert, Bernhard
    Schiffl, Jonas
    Schmitt, Peter H.
    Ulbrich, Mattias
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS (VSTTE 2017), 2017, 10712 : 35 - 48
  • [5] Bottesch R., 2018, LPAR. EPiC Series in Computing, V57, P164, DOI [10.29007/XWWH, DOI 10.29007/XWWH]
  • [6] COMBINING ALGEBRAIC AND ALGORITHMIC REASONING - AN APPROACH TO THE SCHORR-WAITE ALGORITHM
    BROY, M
    PEPPER, P
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1982, 4 (03): : 362 - 381
  • [7] Bubel R., 2007, Verification of Object-Oriented Software. The KeY Approach, P569
  • [8] Formal Specification and Verification of JDK's Identity Hash Map Implementation
    de Boer, Martin
    de Gouw, Stijn
    Klamroth, Jonas
    Jung, Christian
    Ulbrich, Mattias
    Weigl, Alexander
    [J]. INTEGRATED FORMAL METHODS, IFM 2022, 2022, 13274 : 45 - 62
  • [9] Verifying OpenJDK's Sort Method for Generic Collections
    de Gouw, Stijn
    de Boer, Frank S.
    Bubel, Richard
    Haehnle, Reiner
    Rot, Jurriaan
    Steinhoefel, Dominic
    [J]. JOURNAL OF AUTOMATED REASONING, 2019, 62 (01) : 93 - 126
  • [10] de Gouw S, 2016, LECT NOTES COMPUT SC, V10001, P609, DOI 10.1007/978-3-319-49812-6_19
1234