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

Formal Analysis of Concurrent Programs

Armstrong, Alasdair (2015) Formal Analysis of Concurrent Programs. PhD thesis, University of Sheffield.

[img]
Preview
Text
thesis.pdf
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (978Kb) | Preview

Abstract

In this thesis, extensions of Kleene algebras are used to develop algebras for rely-guarantee style reasoning about concurrent programs. In addition to these algebras, detailed denotational models are implemented in the interactive theorem prover Isabelle/HOL. Formal soundness proofs link the algebras to their models. This follows a general algebraic approach for developing correct by construction verification tools within Isabelle. In this approach, algebras provide inference rules and abstract principles for reasoning about the control flow of programs, while the concrete models provide laws for reasoning about data flow. This yields a rapid, lightweight approach for the construction of verification and refinement tools. These tools are used to construct a popular example from the literature, via refinement, within the context of a general-purpose interactive theorem proving environment.

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.686489
Depositing User: Mr Alasdair Armstrong
Date Deposited: 03 Jun 2016 15:39
Last Modified: 03 Oct 2016 13:12
URI: http://etheses.whiterose.ac.uk/id/eprint/13089

Actions (repository staff only: login required)