| ||||
| ||||
![]() Title:Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study Conference:Isabelle 2018 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 ![]() Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study | ||||
Copyright © 2002 – 2025 EasyChair |