Dixon, Alex (2022) Vector addition systems and their applications in the verification of computer programs. PhD thesis, University of Warwick.
Preview |
PDF
WRAP_Theses_Dixon_2022.pdf - Submitted Version - Requires a PDF viewer. Download (1MB) | Preview |
Abstract
Vector Addition Systems (and, equivalently, Petri nets) are a widespread formalism for modelling across a spectrum of problem domains, from logistics to hardware simulation. In this thesis, we firstly explore two classic decidability problems for these models: reachability, whether one can get to a given configuration, and coverability, whether one can exceed it. These problems are sufficent to express a wide class of verification properties for models derived from real-world use cases, including safety and deadlock-freeness. We present and implement a number of approaches for solving both the coverability and reachability problems, including KReach, the first known implementation of a complete decider for the general Petri net reachability problem.
Petri nets offer a natural model of concurrent processes and one of the most common modern use cases for the model is in the verification of safety properties for software, especially sofware with concurrency. In the later half of this work we address some approaches to deciding properties of programs written in Finitary Idealized Concurrent Algol (FICA), a prototypical language combining functional, imperative, and higher-order concurrent programming. We introduce a new family of “leafy” automata models, all based on a novel representation of internal configurations as a tree structure whose semantics is inspired by game-semantic interpretations of FICA terms. We give translations from such terms to our automata and across the work derive decidability of some useful properties for successively more expressive subsets of terms, using a variety of methods including via reachability on Petri nets. We believe these models will help to unify the game- and automata-theoretic views of programming languages and provide a useful basis on which to further study the theory of concurrency.
| Item Type: | Thesis [via Doctoral College] (PhD) |
|---|---|
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software |
| Library of Congress Subject Headings (LCSH): | Petri nets, Distributed parameter systems, Control theory, Machine theory, ALGOL (Computer program language), Parallel programming (Computer science), Computer multitasking, Programming languages (Electronic computers) |
| Official Date: | November 2022 |
| Dates: | Date Event November 2022 UNSPECIFIED |
| Institution: | University of Warwick |
| Theses Department: | Department of Computer Science |
| Thesis Type: | PhD |
| Publication Status: | Unpublished |
| Supervisor(s)/Advisor: | Lazić, Ranko ; Murawski, Andrzej S. |
| Sponsors: | University of Warwick. Centre for Doctoral Training in Urban Science and Progress ; Engineering and Physical Sciences Research Council |
| Format of File: | |
| Extent: | xi, 203 pages : illustrations |
| Language: | eng |
| URI: | https://wrap.warwick.ac.uk/177504/ |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |