Download PDFOpen PDF in browser

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

EasyChair Preprint no. 944

20 pagesDate: April 29, 2019

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: denotational semantics, HOL, Isabelle, program verification, Unifying Theories of Programming

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@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},
  howpublished = {EasyChair Preprint no. 944},
  doi = {10.29007/ddqm},
  year = {EasyChair, 2019}}
Download PDFOpen PDF in browser