I am a research associate at the University of York and working on formal verification of robotics and cyber-physical systems using model checking and theorem proving. I am particularly interested in applying mathematics, logic, and model-based techniques to ensure dependability as computer systems, especially safety-critical systems, are becoming increasingly complex. In my research, I (1) use mathematical logic (alphabetised predicate calculus in Unifying Theories of Programming - UTP) to give (probabilistic) semantics (denotational semantics and operational semantics) to a domain-specific language (RoboChart) in robotics, with support of modelling time and probability, (2) develop automated verification tools using modern model-based techniques (model transformation, validation, and generation) and formal verification (model checking and theorem proving), and (3) apply theoretical semantics and practical tools to a variety of case studies. I am a developer of RoboTool and Isabelle/UTP, the tools developed in our RoboStar group to support modelling and automated verification.
My recent work is summarised in two posters (probabilistic modelling and verification in RoboChart and Formally Verified Animation of RoboChart using interaction trees) and demonstrated (Automated probabilistic verification of RoboChart using PRISM, Animation of the autonomous chemical detector RoboChart model, and Animation of a patrol robot model).
Before I moved to academia in 2012 to pursue a PhD, I have eight years of experience as a senior software and firmware leader in industry: R&D in semiconductor equipment and high-end ToR data centre switches. I have seen some major challenges that traditional software and system engineering is facing: for example, dependability and assurance are not guaranteed. This motivated my interest in formal methods.
Download my CV .
PhD in Computer Science, 2016
University of York