Automated Verification
The automated verification group at Oxford is internationally recognized as among the largest and strongest in the world. Our work spans a wide range of research, from fundamental investigations into the decidability and complexity of model checking for various types of infinite-state systems, through process calculi, logics and semantic models, all the way to practical, machine-assisted methods applicable to real-world problems and programming languages. We also have strong industrial links. Our key strengths include concurrency, abstraction, industrial-scale hardware verification, software model checking, and verification of real-time and probabilistic systems, with applications in security protocols, power management, nanotechnology, and biology. A major source of impact is the adoption by others of verification tools resulting from our research: FDR (model checker), Casper (security protocol compiler), SatAbs (SAT-based model checker for C with predicate abstraction), CBMC (bounded model checker for C) and PRISM (probabilistic model checker). All are highly cited and widely used in industrial contexts, both for research and teaching.
Recent News
Awards
Stefan Kiefer awarded Royal Society University Research Fellowship
For "Quantitative Analysis of Infinite-State Systems" research
Studentships
The Government Communications Headquarters (GCHQ) in Cheltenham has agreed in principle to sponsor a Doctoral Studentship at Oxford University’s Department of Computer Science in the area of Cyber Security.
Related seminar series
Info
People
|
Faculty |
|
|
Visitors |
(University of Warwick)
|
|
Research |
|
|
Students |
|
|
External |
|
|
Administration |
|
|
Past Members |
|
