Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study

EasyChair Preprint 944

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.

Keyphrases: HOL, Isabelle, Unifying Theories of Programming, denotational semantics, program verification

@booklet{EasyChair:944,
  author    = {Joshua Bockenek and Peter Lammich and Yakoub Nemouchi and Burkhart Wolff},
  title     = {Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study},
  doi       = {10.29007/ddqm},
  howpublished = {EasyChair Preprint 944},
  year      = {EasyChair, 2019}}