IRUS Total

Abstraction, refinement and concurrent reasoning

File Description SizeFormat 
Raad-A-2017-PhD-Thesis.pdfThesis4.02 MBAdobe PDFView/Open
Title: Abstraction, refinement and concurrent reasoning
Authors: Raad, Azalea
Item Type: Thesis or dissertation
Abstract: This thesis explores the challenges in abstract library specification, library refinement and reasoning about fine-grained concurrent programs. For abstract library specification, this thesis applies structural separation logic (SSL) to formally specify the behaviour of several libraries in an abstract, local and compositional manner. This thesis further generalises the theory of SSL to allow for library specifications that are language-independent. Most notably, we specify a fragment of the Document Object Model (DOM) library. This result is compelling as it significantly improves upon existing DOM formalisms in that the specifications produced are local, compositional and language-independent. Concerning library refinement, this thesis explores two existing approaches to library refinement for separation logic, identifying their advantages and limitations in different settings. This thesis then introduces a hybrid approach to refinement, combining the strengths of both techniques for simple scalable library refinement. These ideas are then adapted to refinement for SSL by presenting a JavaScript implementation of the DOM fragment studied and establishing its correctness with respect to its specification using the hybrid refinement approach. As to concurrent reasoning, this thesis introduces concurrent local subjective logic (CoLoSL) for compositional reasoning about fine-grained concurrent programs. CoLoSL introduces subjective views, where each thread is verified with respect to a customised local view of the state, as well as the general composition and framing of interference relations, allowing for better proof reuse.
Content Version: Open Access
Issue Date: Sep-2016
Date Awarded: Jun-2017
URI: http://hdl.handle.net/10044/1/49218
DOI: https://doi.org/10.25560/49218
Supervisor: Gardner, Philippa
Drossopoulou, Sophia
Department: Computing
Publisher: Imperial College London
Qualification Level: Doctoral
Qualification Name: Doctor of Philosophy (PhD)
Appears in Collections:Computing PhD theses

Unless otherwise indicated, items in Spiral are protected by copyright and are licensed under a Creative Commons Attribution NonCommercial NoDerivatives License.

Creative Commons