I am Senior Lecturer at the School of Computing Science, University of Glasgow. I obtained a PhD from the same institution with a thesis on bigraphs with sharing, a universal computational model that encapsulates both dynamic and spatial behaviour. You can read my thesis and various academic publications in the Papers section.
My research focusses on the theory of bigraphs and how to use it to reason about safety, reliability and predictability of location-aware, event-based, software systems, particularly complex systems that are already deployed.
I am currently involved in the following research projects:
In the past, I have led the following research projects:
I have also secured funding to conduct research on formal methods for IoT device management platforms, with the Royal Society of Edinburgh and the Taiwan Ministry of Science and Technology, and was visiting researcher at Cambridge and UC Berkeley.
I am the lead developer of BigraphER, a suite of open-source tools for rewriting, simulation and visual display of bigraphs. Recent research includes estimation techniques for networks of sensors with overlapping ranges, digital twinning for Mixed-Reality systems, and human-autonomy teaming in connected vehicular systems. You can find more details in the Research section.
Since 2025, I am a member of the Editorial Board of Science of Computing Programming.
If you are interested in completing a PhD related to my research, then please contact me. You can find information about the application process here.
I am currently recruiting a PhD student on the following topics:This project will focus on the risks and challenges associated with the use of large language models (LLMs) and related generative techniques in environments where trust, accountability, and safety are paramount. Potential applications include policy retrieval, intelligence summarisation, statement transcription and translation, form filling, and statement generation. The project will assess technical risks (e.g. hallucinations) and explore the broader implications of deploying these tools.
This project will develops certified, end-to-end verification methods to raise confidence in PQC algorithms and protocols. The work combines symbolic verification for scalable protocol reasoning with computational proofs for cryptographic soundness, and uses verified toolchains to reduce the trusted computing base. The methodology aims to identify and remove vulnerabilities in PQC-based protocols, provide machine-checked guarantees against quantum adversaries, and support certified implementations suitable for high-assurance deployments.