Mobile menu icon
Skip to navigation | Skip to main content | Skip to footer
Mobile menu icon Search iconSearch
Search type

Department of Computer Science

algebra on a blackboard

Formal methods

Our researchers

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 focussed on the following specialist areas:

  • formal computation model

    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.

  • consumer producer workflow

    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.

  • abstract representation of logic

    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.

  • cryptographic protocol

    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.

  • results table from research paper

    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.

  • formal computational model

    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.

  • abstract ontology representation

    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.

  • abstract from research paper

    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.