Latest News See my paper on Exploring the Boundaries of Rely/Guarantee and Links to Linearisability and
my paper with Cliff Jones: Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols, published in the 22nd International Overture Workshop.
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.
At ANU, I'm currently looking at techniques for the verification of security protocols, working with Prof. Cliff Jones at Newcastle University, U.K. I'm also interested in the foundations of concurrency. My latest research in this area has been
on the links between rely/guarantee reasoning and linearisability for non-blocking algorithms.
Previously, I was a Senior Lecturer at De Montfort University, Leicester, U.K. I taught Data Structures & Algorithms and Concurrent & Parallel Algorithms
to 2nd year students. I was also Deputy Programme Leader of the BSc Computer Science & BSc Software Engineering degrees.
From 2013 to 2017 I worked at Newcastle University in the UK on the
Taming Concurrency project. This project aimed 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.
Before that, in my hometown Brisbane, I worked on several projects
at Griffith University and The University of Queensland (UQ) from 2004 to 2007, 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 .
