A Verified Timsort C Implementation in Isabelle/HOL
This provides a verified Timsort for C programmers, but it is incremental as it builds on existing verification work in other languages.
The paper tackled the lack of a standard formally verified Timsort implementation in C by developing one using Isabelle/HOL and Simpl, resulting in a C implementation tested with random cases.
Formal verification of traditional algorithms are of great significance due to their wide application in state-of-the-art software. Timsort is a complicated and hybrid stable sorting algorithm, derived from merge sort and insertion sort. Although Timsort implementation in OpenJDK has been formally verified, there is still not a standard and formally verified Timsort implementation in C programming language. This paper studies Timsort implementation and its formal verification using a generic imperative language - Simpl in Isabelle/HOL. Then, we manually generate an C implementation of Timsort from the verified Simpl specification. Due to the C-like concrete syntax of Simpl, the code generation is straightforward. The C implementation has also been tested by a set of random test cases.