Andrew Cook Undergraduate Dissertation 2016/17

Verifying the Correctness of Sorting Algorithms in Isabelle/HOL

Supervised by G.Struth

Abstract

This paper aims to show formal verification of the correctness of common, non-recursive sorting algorithms using the Higher Order Logic (HOL) theorem prover Isabelle in conjunction with Hoare logic and Kleene Algebra with tests. Background context of the underlying mathematical concepts, as well as descriptions and simple demonstrations of the verification components used, are also included. Partial correctness verification semantics are considered for the scope of this project, and total correctness is not considered in this dissertation. This project aims to be an introduction to automated reasoning of systems using an interactive proof assistant. Sorting algorithms Bubble Sort and Insertion Sort are shown in this paper to be partially correct. Lastly, this paper outlines further work for this project that will be considered.