White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Algebraic Principles for Program Correctness Tools in Isabelle/HOL

Borges Ferreira Gomes, Victor (2015) Algebraic Principles for Program Correctness Tools in Isabelle/HOL. PhD thesis, University of Sheffield.

Text (Access to Thesis Form)
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (1159Kb) | Preview
Text (PhD Thesis)
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (892Kb) | Preview


This thesis puts forward a flexible and principled approach to the development of construction and verification tools for imperative programs, in which the control flow and the data level are cleanly separated. The approach is inspired by algebraic principles and benefits from an algebraic semantics layer. It is programmed in the Isabelle/HOL interactive theorem prover and yields simple lightweight mathematical components as well as program construction and verification tools that are themselves correct by construction. First, a simple tool is implemented using Kleeene algebra with tests (KAT) for the control flow of while-programs, which is the most compact verification formalism for imperative programs, and their standard relational semantics for the data level. A reference formalisation of KAT in Isabelle/HOL is then presented, providing three different formalisations of tests. The structured comprehensive libraries for these algebras include an algebraic account of Hoare logic for partial correctness. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. Second, the tool is expanded to support different programming features and verification methods. A basic program construction tool is developed by adding an operation for the specification statement and one single axiom. To include recursive procedures, KATs are expanded further to quantales with tests, where iteration and the specification statement can be defined explicitly. Additionally, a nondeterministic extension supports the verification of simple concurrent programs. Finally, the approach is also applied to separation logic, where the control-flow is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data level is captured by concrete store-heap models. These are linked to the algebra by soundness proofs. A number of examples shows the tools at work.

Item Type: Thesis (PhD)
Academic Units: The University of Sheffield > Faculty of Engineering (Sheffield) > Computer Science (Sheffield)
The University of Sheffield > Faculty of Science (Sheffield) > Computer Science (Sheffield)
Identification Number/EthosID: uk.bl.ethos.682305
Depositing User: Mr Victor Borges Ferreira Gomes
Date Deposited: 11 Apr 2016 08:00
Last Modified: 03 Oct 2016 13:10
URI: http://etheses.whiterose.ac.uk/id/eprint/12457

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)