Formally Verifying an Efficient Sorter

In this experience report, we present the complete formal verification of a Java implementation of inplace superscalar sample sort (ips4o) using the KeY program verification system. As ips4o 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.