Tags:Denotational Semantics, HOL, Isabelle, Program Verification and Unifying Theories of Programming
Abstract:
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.
Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study