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

Software Model Checking Manual inspection of complex software is error-prone and costly, and …

Read more about Software Model Checking

All Projects

Projects

Reasoning about control To reason about linear systems expressed as block diagrams that give a graphical represen…

Read more about Reasoning about control

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