Research at OUCL is classified into seven broad themes. This
provides a map of the research landscape of the Laboratory for public
presentation of our work. The themes also help to structure our
research management: each researcher is nominally assigned a primary
theme, according to research interests; each theme has a head, who has
general oversight of its work.
Within (and across) themes, research is conducted by
teams of people, or individually, as best suits the staff, the
topic, and the funding. If the research has a specific
target, or an end-date, then it is presented here as a
project; otherwise, it is presented as an activity. Most
activities are focussed around a named research group or a
funded research centre.
The Department's research activity was evaluated in the most
recent Research Assessment Exercise (RAE2008),
published in December 2008. 80% of the submitted researchers
were found to be in the top two tiers, either 4*
(world-leading) or 3* (internationally excellent). A more
detailed analysis is
available.
Verification
The 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.