Since June 2022, I am a Research Fellow at the School of Physics, Engineering and Technology at the University of York, UK. I am a member of the RoboStar Centre of Excellence in Software Engineering for Robotics, and currently working for the EPSRC-funded RoboTest project, which seeks to develop model-based testing approaches tailored for simulation and testing of robots.
Previously, I was a Research Associate on the EPSRC-funded RoboCalc project at the Department of Computer Science. I have also previously worked on the theoretical underpinnings of Safety-Critical Java as part of the EPSRC-funded hiJaC project.
My research interests concern the formal specification and verification of cyber-physical and autonomous systems. I am interested in the development of model-based approaches for specification, namely using domain-specific languages, and in the use of heterogeneous semantics to capture a wide range of phenomena, such as data modelling, time, concurrency and continuous behaviour.
With regards to formal semantics, I am interested in denotational and algebraic approaches, as featured, for example, in the alphabetised relational algebra of Hoare and He’s Unifying Theories of Programming. I also have significant experience working with (timed) process calculi, including, Circus, Communicating Sequential Processes (CSP) and their timed variants, namely tock-CSP [1], a discrete timed-model.
From a practical point of view, I am interested in efficient approaches to verification, namely using model-checking and interactive theorem proving. My tools of the trade are FDR4 and Isabelle, including Isabelle/UTP.
This is my departmental website where I publish my technical work amongst other bits of information. Please feel free to get in touch if you would like to know more about my work.