Skip to main content

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.

Related seminar series

All Activities

Activities

Concurrency Oxford has long been one of the main centres of concurrency research.…

Read more about Concurrency

RECOUNT Recursions arise naturally when writing programs. They can be natural…

Read more about RECOUNT

All Projects

Projects

AFFECTech To support self-understanding and successful adoption of adaptive emotion regulation stra…

Read more about AFFECTech

Mobile Robotics To create, run and exploit the world's leading research programme in mobile autonomy, add…

Read more about Mobile Robotics

All Publications

Publications

A Survey of Automated Techniques for Formal Software Verification

Read more about A Survey of Automated Techniques for Formal Software Verification

Scoot: A Tool for the Analysis of SystemC Models

Read more about Scoot: A Tool for the Analysis of SystemC Models

Research