I've been a researcher in formal methods since 2004. My research interests are in the verification of systems which exhibit a high degree
of complexity, making them prone to errors and difficult to verify. I am particularly interested in safety-critical systems, which can potentially
have serious impact. My research explores the various challenges associated with such systems, including methods to handle the concurrency aspects
and methods for conducting failure analyses on systems that include potentially faulty hardware components.
I'm currently a lecturer at De Montfort University in Leicester, U.K. Visit my staff page.
From 2013 to 2017 I worked at Newcastle University in the UK on the
Taming Concurrency project. This project aims to investigate the fundamental aspects of concurrency, comparing the various methods for handling
concurrency in order to extract an understanding of these core aspects. With Cliff Jones, I published a paper at SEFM 2015 (see below), which explores
the use of abstraction for handling problems with strong separation of components, providing an alternative approach to the common separation logic methods.
This abstraction solution helps to shed light on the fundamental qualities of separation. Similarly, we are now investigating a concurrent garbage-collection
algorithm using rely-guarantee methods, in an attempt to understand the underlying qualities exhibited by such systems.
Read the relevant papers here.
Previously, in my hometown Brisbane, I worked on several projects
at Griffith University and The University of Queensland (UQ), as part of the ARC Centre for Complex Systems, on the verification of safety-critical systems
using the Behavior Tree specification language, a language which maintains strong links between the natural language requirements and the formal model. My research
focussed on using Behavior Trees and model checking to automate safety analyses. Read the relevant papers here.
My PhD thesis (obtained in 2012 from Griffith University, supervised by Kirsten
Winter from UQ and Geoff Dromey at the start) is on the use of slicing techniques to reduce Behavior Tree models prior to model checking, to allow large systems to be verified.
I also developed a novel form of branching bisimulation, called Next-preserving Branching Bisimulation, which allows stuttering behaviour to be removed while still preserving
full CTL*, including the Next operator (see my journal paper listed below). Read the relevant papers or download my thesis here.
Following my PhD studies, I applied the failure analysis technique to an air-traffic
control system for a project at UQ funded by NICTA.
Details of these projects can be found on my projects page.
See my papers or my thesis .
Reasoning about Separation using Abstraction and Reification with Cliff B. Jones published in SEFM 2015
Next-preserving Branching Bisimulation with Kirsten Winter published in Theoretical Computer Science.
For details of both and to watch the Audioslides presentation for the TCS paper, see my papers page.