Implementation and Verification of Sorting Algorithms with the Interactive Theorem Prover HOL

Sammanfattning: As the world becomes increasingly reliant on technology and the technology becomes increasingly complex, ensuring software correctness is becoming both increasingly important and difficult. Methods like software testing are rarely enough to guarantee that a program will always work as intended. Formal methods offer attractive alternatives. Using formal methods, properties about software can be unambiguously proven for all possible input. In this project we use the interactive theorem prover HOL to define and formally verify a simplified version of the popular sorting algorithm Timsort. We also formalize the time-complexity property and prove the best-case time-complexity of the simplified algorithm. We intended to use the CakeML compiler to generate verified machine code from the HOL definitions, and thus produce an end-to-end verified executable program. Because of time constraints, we instead generated ML code using EmitML. The resulting ML code is not guaranteed to retain the proven properties during execution. The project demonstrates how sorting algorithms can be formally verified and provides parts that could be re-used to verify the actual Timsort algorithm.