Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study
Joshua A. Bockenek, Peter Lammich, Yakoub Nemouchi, Burkhart Wolff · EasyChair preprint · 2019
We verify functional correctness of insertion sort as well as the partition function of quicksort. We use Isabelle/UTP and its denotational semantics for imperative programs as a verification framework. We propose a forward Hoare VCG for our reasoning and we discuss the different technical challenges encountered while using Isabelle/UTP.