Repository logo
 

Concurrent verification for sequential programs


No Thumbnail Available

Type

Thesis

Change log

Authors

Wickerson, John Peter 

Abstract

This dissertation makes two contributions to the field of software verification. The first explains how verification techniques originally developed for concurrency can be usefully applied to sequential programs. The second describes how sequential programs can be verified using diagrams that have a parallel nature. The first contribution involves a new treatment of stability in verification methods based on rely-guarantee. When an assertion made in one thread of a concurrent system cannot be invalidated by the actions of other threads, that assertion is said to be 'stable'. Stability is normally enforced through side-conditions on rely-guarantee proof rules. This dissertation proposes instead to encode stability information into the syntactic form of the assertion. This approach, which we call explicit stabilisation, brings several benefits. First, we empower rely-guarantee with the ability to reason about library code for the first time. Second, when the rely-guarantee method is redepleyed in a sequential setting, explicit stabilisation allows more details of a module's implementation to be hidden when verifying clients. Third, explicit stabilisation brings a more nuanced understanding of the important issue of stability in concurrent and sequential verification; such an understanding grows ever more important as verification techniques grow ever more complex. The second contribution is a new method of presenting program proofs conducted in separation logic. Building on work by Jules Bean, the ribbon proof is a diagrammatic alternative to the standard 'proof outline'. By emphasising the structure of a proof, ribbon proofs are intelligible and hence useful pedagogically. Because they contain less redundancy than proof outlines, and allow each proof step to be checked locally, they are highly scalable; this we illustrate with a ribbon proof of the Version 7 Unix memory manager. Where proof outlines are cumbersome to modify, ribbon proofs can be visually manoeuvred to yield proofs of variant programs. We describe the ribbon proof system, prove its soundness and completeness, and outline a prototype tool for mechanically checking the diagrams it produ1res.

Description

This thesis is not available on this repository until the author agrees to make it public. If you are the author of this thesis and would like to make your work openly available, please contact us: thesis@repository.cam.ac.uk.


Cambridge University Library can make a copy of this work available only for the purposes of private study and non-commercial research. Copies should not be shared or saved in any shared facilities. Copyright over the content of these works is with their authors. Theses from the Library collection are considered unpublished works and according to UK legislation quoting from them is not allowed without permission from their author.

If you can commit to these terms, please complete the request form which you can find through this link: https://imagingservices.lib.cam.ac.uk/


Please note that print copies of theses may be available for consultation in the Cambridge University Library's Manuscript reading room. Admission details are at http://www.lib.cam.ac.uk/collections/departments/manuscripts-university-archives

Date

Advisors

Keywords

Qualification

Doctor of Philosophy (PhD)

Awarding Institution

University of Cambridge