Formal methods

Our expertise covers a broad span of topics in formal methods, automated reasoning, logic and theory.

Our research provides practical tools and theoretical foundations in a variety of areas in Artificial Intelligence and Computer Science, including specification and verification of hardware, software and agent systems; cryptography; knowledge representation, reasoning and support for knowledge management; programming language research; and new mathematics of computational behaviour.

We are world-leading in the automation of logic and the development of automated reasoning tools across several areas.

Research focus

Our research is focused on the following specialist areas:

• 

  Automated reasoning

  The automation of reasoning without human intervention is one of the long-standing goals of computer science. We combine theoretical foundations with sophisticated engineering to develop reasoning methodologies used across several areas such as: automated verification, security analysis, ontology engineering and large theories. From this we produce award-winning, industrial-strength, automated theorem provers.

• 

  Automated verification

  Automated verification gives us tools to demonstrate correctness with strong mathematical guarantees of complex hardware and software systems. We focus attention on algorithm verification, verified information, flow in web applications, the verification of smart contracts, and on the punishment (not reward) blockchain architecture.

• 

  Computational logic

  Computational logic provides practical and theoretical foundations over a variety of areas of computer science and AI but also cognitive science and computational linguistics. Our expertise focuses on spatial logics, modal and description logics, on decidability and complexity problems of fragments of first-order logic, and on the logical analysis of fragments of natural language.

• 

  Knowledge extraction and reasoning

  Ontologies and automated reasoning provide key technology for AI in health, where they provide the basis for medical terminological services used in health care sectors across the world to allow consistent data capture, easy data sharing, and convenient access, querying and analysis of data. We develop tools to support the automatic knowledge extraction and sharing for medical ontologies based on subontology generation, forgetting and modularisation with applications for ontology difference tracking, information hiding, abductive learning, hypothesis generation, knowledge sharing among agents and query answering.

• 

  Mathematical models for proofs and programs

  Both formal derivations and programs are descriptions of procedures in some syntactic system. Comparing such procedures is difficult, and the aim of using mathematical models is to provide an infrastructure for doing so. We work on developing and describing such models and investigating their properties.

• 

  Program analysis

  Program analysis investigates the theory and practice of automatically analysing the behaviour of software systems with respect to a given property. We focus on model checking, abstract interpretation and runtime verification, with applications in security for cyber-controls, robotics, industrial control systems and the internet of things.