This artifact zip contains the proof and evaluation material for thefollowing contribution to the TACAS 2024 conference: Formally Verifying an Efficient Sorter by Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler, and Sascha Witt The material contained in this archive was used in1) the deductive program verification proofs conducted in KeY and2) the empirical evaluation regarding the performance of the sorting algorithm. This artifact is intended to be run inside the TACAS 2023 virtualmachine [1]. In order to be able to use the artifact, some moresoftware needs to be installed. Copy this archive into the VM, unzipit and execute sudo bash setup.sh from the directory in which this README.txt resides. It will install aJava 21 runtime, the SMT solver Z3, ant and a bit more. Afterwards you can head to the directory ips4o-verify/ for the KeYproofs and to ips4o-java-benchmark/ for the empirical evaluation. KeY proofs---------- This is a snapshot of the repository https://github.com/KeYProject/ips4o-verify In order to replay all KeY proofs, you can invoke "make check" in thesubdirectory ips4o-verify/ on the CLI. The JML annotated Java sources that have been verified are located inthe directory "src/main/java". When executed in an environment which has a GUI option, the tool canalso be run interactively using "make run" or "make run-overflow".(On the CLI a number of "project.key" files will be suggestes whichare good starting points for loading proof obligations, one can alsoload ".proof" files from src directory. Since there are two toolversions involved, be sure to use "make run-overflow" for the filesinside "key-overflow" and "make run" for the directory "key"). For further information see the README inside the repository. Empirical evaluation-------------------- This is a snapshot of the repository https://github.com/SaschaWitt/ips4o-java-benchmark(with a modified symbolic link) You need to run ant from inside the directory ips4o-java-benchmark/. Further informationcan be found in the README there. [1] G. Fedyukovich and S. Mover, “TACAS 23 Artifact Evaluation VM -Ubuntu 22.04 LTS”. Zenodo, Sep. 26, 2022. doi: 10.5281/zenodo.7113223.