Andreas Theocharous Undergraduate Dissertation 2016/17

Verification and Correctness of Sorting Algorithms in Isabelle/HOL

Supervised by G.Struth

Abstract

Studies on how computer programs may be formalised in mathematical models and verified have been drawing the interest of computer scientists for the past few decades. An examination of program verification methods is provided here along with an introduction on the interactive theorem prover Isabelle which supports automated theorem proving. Ways of implementing these logical models and using them to prove simple algorithms in Isabelle's environment are presented and compared. The way of using these implementations to express and verify algorithms is demonstrated through the verification of the proofs of three sorting algorithms as well as other simple examples.