Formally Verifying an Efficient Sorter.

In this experience report, we present the complete formal verification of a Java implementation of inplace superscalar sample sort ( [inline-graphic not available: see fulltext]) using the KeY program verification system. As [inline-graphic not available: see fulltext] 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.