Mobile menu icon
Mobile menu icon Search iconSearch
Search type

School of Computer Science

Abstract image of equations

Theory and foundations

Our research covers a wide spectrum of computational and algorithmic principles, quantitative and symbolic techniques, models and mathematical techniques in computer science.

Our facilities

We boast an incredible array of facilities, making our innovative theory and foundations research possible.

It provides the underpinning and deep understanding of computational behaviour, for example, correctness, termination properties, complexity and optimisation, of transition systems providing foundations for software and hardware systems, relationships between systems, of language design principles, of data relevant issues and so on.

In fact, every aspect of computer science has rich theory and computational foundations: program language semantics, modelling of software and hardware systems, databases, security and cryptography, all areas of artificial intelligence, including machines learning, knowledge representation and reasoning and natural language processing.

Across these areas our focus is both on theory from practice and development of techniques and tools with strong theoretical and computational foundations.

Areas of expertise

Our researchers focus their work in the following specialist areas:

  • Robotic arms working on assembly line

    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.

    Contact: Giles Reger

  • Close-up of woman's eye looking at transparent screen

    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.

    Contact: Giles Reger

  • Close-up of abstract php code on black screen

    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.

    Contact: Giles Reger

  • Close-up of abstract php code on white screen


    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.

    Contact: Mustafa Mustafa

  • Code on a computer screen

    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.

  • Computer generated image of brain on navy background

    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.

  • Hand using a keyboard behind a wall of data

    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.

    Contact: Lucas Cordeiro

Postgraduate research projects

Richard Banach projects

Lucas Cordeiro projects

Dirk Koch projects

Peter Lammich projects

Mustafa Mustafa projects

Giles Reger projects

Rizos Sakellariou projects

Andrea Schalk projects

Carole Twining projects