Automated Verification
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.