Formal methods

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

Our research provides practical tools andtheoretical 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 focussed 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, flowing 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.

• 

  Cryptography

  Cryptography investigates the theory and practice of ensuring secure communication of computer-based systems by constructing and analysing protocols to prevent adversaries from reading private messages. We focus on formally verifying security properties of both abstract models and code implementing cryptographic protocols by combining abstract interpretation, symbolic execution and fuzzing.

• 

  Formal system modelling and development

  Much of the complexity of system development can be mastered via a top-down approach. When suitably formalised, increasingly detailed properties can be accumulated and reasoned about. We apply this refinement-oriented approach particularly to awkward system requirements and cyber-physical systems via the Hybrid Event-B methodology.

• 

  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.

• 

  Ontology re-engineering

  Ontologies provide structured representation of large knowledge bases used, for example, in the healthcare and biomedical sectors, the semantic web and artificial intelligence. We are leading the development of tools for re-engineering in ontologies such as modularisation and abstraction, difference tracking, information hiding and hypothesis generation.

• 

  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.