We develop systematic tools, theories, and methodologies for ensuring the correctness, reliability, and efficiency of software and systems, focusing on automated techniques such as model checking, machine learning, and program analysis. We target several different challenging kinds of software and systems, ranging from (concurrent) object-oriented programs to real cyber-physical systems such as SWaT.
This page provides an overview of some of our research projects. For more information, please take a look at our publications.
- PAT: Process Analysis Toolkit — a self-contained framework that supports composing, simulating, and reasoning about domains including concurrent and real-time systems.
Applied Machine Learning
- ALearner — learns likely assertions based on passing and failing test cases.
- TLV — combines testing, learning, and validation to construct correct and accurate abstractions of Java classes.
- Tzuyu — automatically learns stateful typestates through active learning.
- ZiQian — automatically learns probabilistic models from system executions.
- Ziyuan — applies bug localisation and active learning to construct “simple” predicates explaining why test cases are failing.
- Lock and Immutability Checkers — tools for checking issues related to locking and immutability in Java.
Hybrid Systems Analysis
- HyChecker — analyses hybrid systems using a combination of random sampling and symbolic execution (“concolic sampling”).
Attestation of Cyber-Physical Systems
- Physical Attestation — learning invariants of cyber-physical systems from the traces of mutated PLC software, and applying them to attest the system.
Verification of Security Protocols
- Timed and Parameterised Security Protocol Verification — comprehensive analysis framework to formally specify and automatically verify timed security protocols.