The automated verification theme investigates theory and practice of formal verification and correct-by-construction synthesis
for software and hardware systems. Our work spans a wide range of research, from studying decidability and complexity, through
formulating process calculi, logics, semantic models and abstraction schemes, all the way to practical, machine-assisted methods
applicable to real-world problems and programming languages such as C and Java. We focus on model checking, control and synthesis
problems for concurrent, probabilistic, real time, hybrid, dynamical and infinite-state systems, with applications in security,
mobile robotics, energy management, wearable devices, web services, molecular computation, nanotechnology, and biology. A
number of widely used verification tools have resulted from our research, including
FDR (model checker), CBMC (bounded model
checker for C) and PRISM (probabilistic model checker).
The theme has recently spun out a company, DiffBlue, that aims to automate coding tasks such as testing and bug fixing.
Related seminar series