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 challenge...
Research Assistant
AI chat, annotations, notes & similar papers
No comments yet
Be the first to share your thoughts!