FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study

Authors: Joshua Bockenek, Peter Lammich, Yakoub Nemouchi and Burkhart Wolff

PapersPapers with AbstractsPrefaceAuthor IndexKeyword Index

Paper Information

Title:Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study
Authors:Joshua Bockenek, Peter Lammich, Yakoub Nemouchi and Burkhart Wolff
Proceedings:Isabelle Papers
Editor: Makarius Wenzel
Keywords:Unifying Theories of Programming, HOL, Isabelle, Program Verification, Denotational Semantics
Abstract:

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.

Pages:20
Talk:Jul 13 17:00 (Session 88C: Isabelle 4)
Paper: