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:
-
Autonomy and verification
The Autonomy and Verification Group focuses on autonomous systems and their development, verification, and analysis.
Read more
-
Formal methods
We provide formal mathematical foundations for Computer Science, from verification of hardware, software and agent systems to cryptography and knowledge representation, reasoning and knowledge management.
Read more
-
Information management
We design, develop and build state of the art data and knowledge management systems -- spanning from formal underpinnings in knowledge representation and logic, to challenging interdisciplinary work.
Read more
-
Systems and software security
We develop state-of-the-art algorithms, methods and protocols to address security and privacy in networked and distributed system environments, and tools to build verifiable, trustworthy software systems.
Read more
Postgraduate research projects
Theory and foundations projects
- A Multi-Tenancy FPGA Cloud Infrastructure and Runtime System
- Application Level Verification of Solidity Smart Contracts
- Automated Repair of Deep Neural Networks
- Automatic Detection and Repair of Software Vulnerabilities in Unmanned Aerial Vehicles
- Blockchain-based Local Energy Markets
- Categorical proof theory
- Combining Concolic Testing with Machine Learning to Find Software Vulnerabilities in the Internet of Things
- Exploiting Software Vulnerabilities at Large Scale
- Finding Vulnerabilities in IoT Software using Fuzzing, Symbolic Execution and Abstract Interpretation
- Formal Methods: Hybrid Event-B and Rodin
- Formal Methods: Mechanically Checking the Semantics of Hybrid Event-B
- Formal Semantics of the Perfect Language
- Formal Verification for Robot Swams and Wireless Sensor Networks
- Formal Verification of Robot Teams or Human Robot Interaction
- Foundations and Advancement of Subontology Generation for Clinically Relevant Information
- Generative AI for Video Games
- Hybrid Fuzzing Concurrent Software using Model Checking and Machine Learning
- Machine Learning with Bio-Inspired Neural Networks
- Mathematical models for concurrent systems
- Neuro-sybolic theorem proving
- Optimization and verification of systems modelled using neural networks
- Problems in large graphs representing social networks
- Security and privacy in p2p electricity trading
- Software verification with contrained Horn clauses and first-order theorem provers
- Solving PDEs via Deep Neural Nets: Underpinning Accelerated Cardiovascular Flow Modelling with Learning Theory
- Solving mathematical problems using automated theorem provers
- Solving non-linear constraints over continuous functions
- Symmetries and Automated Theorem Proving
- Theorem Proving for Temporal Logics
- Trustworthy Multi-source Learning (2025 entry onward)
- Using Program Synthesis for Program Repair in IoT Security
- Verifying Cyber-attacks in CUDA Deep Neural Networks for Self-Driving Cars
Richard Banach projects
Ke Chen projects
- Automatic Activity Analysis, Detection and Recognition
- Automatic Emotion Detection, Analysis and Recognition
- Biologically-Plausible Continual Learning
- Contextualised Multimedia Information Retrieval via Representation Learning
- Deep Learning for Temporal Information Processing
- Ensemble Strategies for Semi-Supervised, Unsupervised and Transfer Learning
- Explainable and Interpretable Machine Learning
- Generative AI for Video Games
- Machine Learning and Cognitive Modelling Applied to Video Games
- Multi-task Learning and Applications
- Music Generation and Information Processing via Deep Learning
- Zero-Shot Learning and Applications
Lucas Cordeiro projects
- Application Level Verification of Solidity Smart Contracts
- Automated Repair of Deep Neural Networks
- Automatic Detection and Repair of Software Vulnerabilities in Unmanned Aerial Vehicles
- Combining Concolic Testing with Machine Learning to Find Software Vulnerabilities in the Internet of Things
- Designing Safe & Explainable Neural Models in NLP
- Exploiting Software Vulnerabilities at Large Scale
- Finding Vulnerabilities in IoT Software using Fuzzing, Symbolic Execution and Abstract Interpretation
- Hybrid Fuzzing Concurrent Software using Model Checking and Machine Learning
- Using Program Synthesis for Program Repair in IoT Security
- Verification Based Model Extraction Attack and Defence for Deep Neural Networks
- Verifying Cyber-attacks in CUDA Deep Neural Networks for Self-Driving Cars
Clare Dixon projects
Marie Farrell projects
Alejandro Frangi projects
Michael Fisher projects
Samuel Kaski projects
- Automatic Experimental Design with Human in the Loop (2025 entry onward)
- Collaborative Probabilistic Machine Learning (2025 entry onward)
- Learning of user models in human-in-the-loop machine learning (2025 entry onward)
- Probabilistic modelling and Bayesian machine learning (2025 entry onward)
- Trustworthy Multi-source Learning (2025 entry onward)
Dirk Koch projects
Konstantin Korovin projects
- Neuro-sybolic theorem proving
- Optimization and verification of systems modelled using neural networks
- Software verification with contrained Horn clauses and first-order theorem provers
- Solving mathematical problems using automated theorem provers
- Solving non-linear constraints over continuous functions
- Symmetries and Automated Theorem Proving
Tingting Mu projects
Anirbit Mukherjee projects
Mustafa Mustafa projects
Pavlos Petoumenos projects
Oliver Rhodes projects
Giles Reger projects
Rizos Sakellariou projects
- Dynamic Resource Management for Intelligent Transportation System Applications
- Finding a way through the Fog from the Edge to the Cloud
- Job and Task Scheduling and Resource Allocation on Parallel/Distributed systems including Cloud, Edge, Fog Computing
- Managing the data deluge for Big Data, Internet-of-Things and/or Industry 4.0 environments
- Problems in large graphs representing social networks
- Scheduling, Resource Management and Decision Making for Cloud / Fog / Edge Computing
