Automata-theoretic approaches to game semantics and formal verification

Lead Research Organisation: University of Bristol
Department Name: Computer Science

Abstract

Over the course of my MEng degree at Warwick, I have become deeply interested in the theories of automata and programming languages. As the core of my PhD research, I intend to explore the intersection of both of these areas, applying automata theory (particularly infinite-alphabet automata) and game semantics to investigate the properties of programming languages and other computational models, with the aim of finding subsets of these models that are well-suited to formal verification techniques. The intersection of automata theory and game semantics was first explored by Abramsky et al. in 2004 [1]. In this paper, the game semantics of a simply-typed toy language was modelled using regular expressions; this equivalence was then used to construct a formal verification tool for the language. This direction was further investigated by Dixon et al. in 2021 [9, 10]. In this work, a class of infinitealphabet tree automata (leafy automata) was introduced and used to model the game semantics of Finitary Idealised Concurrent Algol (Fica) [13], a toy language with features corresponding to concurrency (multiple threads, semaphores, etc.). It was shown that every Fica term can be converted into a leafy automaton whose trace models the semantics of the term. This equivalence, as well as the decidability of a certain subclass of leafy automata, was then used to find a subset of Fica that is particularly susceptible to formal verification.

Publications

10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/W524414/1 30/09/2022 29/09/2028
2926279 Studentship EP/W524414/1 30/09/2024 30/03/2028 THOMAS DIVERS