Project List

A Cyclic Prover for Propositional Dynamic Logic (available)

Propositional Dynamic Logic (PDL) [1] is a logic in which abstract properties about the behaviour of programs can be expressed, in a very general way. Because of its generality it is suitable for checking the behaviour or a wide range of programs and systems, via model checking. PDL is what is known as a modal … full description “A Cyclic Prover for Propositional Dynamic Logic (available)”

A tool for annotating materials with the ontology terms4FAIRskills (available)

term4FAIRskills is an ontology to describe the necessary skills to make data FAIR and keep FAIR. FAIR itself is a set of principles for ensuring that data is shared in as efficient and effective a manner as possible. In the field of Data Science there are colloquial estimates that perhaps 80% of the time spent … full description “A tool for annotating materials with the ontology terms4FAIRskills (available)”

A tool for testing global accessibility of open data resources (available)

Research depends on data that is openly available. Recently, it has become clear that access to repositories that store these data sets is variable across the country that accesses the data. This can be due to poor connectivity for Lower income countries to countries that are actively blocked from accessing specific sites. A set of … full description “A tool for testing global accessibility of open data resources (available)”

A Toolkit for Micro-architectural Attacks on Mobile Devices (available)

Micro-architectural attacks leverage side-effects from modern processor features during the execution of secret-dependent code. These attacks have emerged in recent years as a potent vector for recovering cryptographic keys and other secret data. Despite this, very few implementations of published attacks have been released publicly on mobile devices, which has raised questions about their reproduciblity. … full description “A Toolkit for Micro-architectural Attacks on Mobile Devices (available)”

A Web interface to the ART software language engineering toolkit (available)

ART is a software tool developed with the Centre for Software Language Engineering which addresses a spectrum of modern programming language technologies, including generalised parsing, attribute grammar evaluation and executable formal semantics specifications. ART is used extensively in our course CS3480 Software Language Engineering and will shortly be released for general use. We would like to … full description “A Web interface to the ART software language engineering toolkit (available)”

Algorithmic Game Theory and Computational Social Choice (available)

This project will be co-supervised with Eduard Eiben. We will study a topic arising from Algorithmic Game Theory and/or Computational Social Choice. The specific topic/area will be defined during an inital meeting with Eduard and myself. Some examples of such topics are (this list is by no means exhaustive):– Computation of Nash Equilibria;– Fair Division … full description “Algorithmic Game Theory and Computational Social Choice (available)”

Algorithms for Temporal Graphs (available)

The project will be co-supervised with Argyris Deligkas. The focus of the project is to study and optimize real-life networks that change over time. Some prominent examples of such networks include logistics schedules, public transportation systems, electricity-demand over power grids, information flows, and virus spreading. We plan to study this type of problems through the … full description “Algorithms for Temporal Graphs (available)”

Automated verification of CPU branch-predictors (available)

Branch predictors are components of CPUs that try to guess the outcome of a branching statement (e.g., an if-then-else) before it is known. They speed up the flow of instructions in the instruction pipeline by “pre-executing” what comes after a branching statement, and they play a key role in achieving high performance in modern CPUs. … full description “Automated verification of CPU branch-predictors (available)”

Automated verification of Rowhammer mitigations (available)

Rowhammer [1], first introduced in [2], is a security exploit that relies on electromagnetic side-effects happening in DRAM memories due to repeated accesses to the same row(s) in a short period of time. In fact, accessing the same row in the DRAM many times in a short span of time may cause electromagnetic interactions with … full description “Automated verification of Rowhammer mitigations (available)”

Autonomous Cars – Evaluation of Security Countermeasures (available)

Project Description Autonomous and connected vehicles will be a part of reality in the near future. There are many development efforts currently underway to pave the way for the deployment of autonomous vehicles (self-driving cars) in public areas. These vehicles are a collection of complex and sophisticated computational architectures. Cybersecurity is among many challenges that … full description “Autonomous Cars – Evaluation of Security Countermeasures (available)”

Binary Neural Networks in C (available)

Neural Networks (NNs) are powerful and popular machine learning models used in natural and social sciences and various commercial frameworks. Their strengths come from the potentially-large flexibility and the possibility of training them through scalable methods, e.g. stochastic gradient descent. On the other hand, trained NNs have a huge memory footprint, as millions of real-valued … full description “Binary Neural Networks in C (available)”

Building a chatbot for student queries (available)

It is important that student queries are replied to quickly and accurately. Many of the requests for information are fully explained in resources such as the student handbook. These include questions such as where students request extensions on coursework or how shuold they inform College if they are absent from a lecture. Frequently these questions … full description “Building a chatbot for student queries (available)”

Carbon Labelling – Blockchain based product carbon footprint system. (available)

Project Description Carbon footprint associated with a product is a combination of the emission-related in the manufacturing and logistics of the product. Logistics plays a vital role in moving products from factories to home and is one of the significant causes of carbon emission in Europe. Besides this, the last mile delivery network is also … full description “Carbon Labelling – Blockchain based product carbon footprint system. (available)”

Combatting Fake News Using Mobile Trusted Execution Environments (available)

The distribution of fake news – hoaxes, propaganda, and outright false articles – by pseudo-news outlets is a major issue. Fake news can undermine trust in legitimate sources of news and the integrity of the democratic process. Existing methods to combat this issue have significant shortcomings. Manual take-downs are slow and lack scalability, particularly if … full description “Combatting Fake News Using Mobile Trusted Execution Environments (available)”

Computer Vision for Extreme Environments (available)

The use of data from extreme environments in computer vision have shown an increase of interest in recent years as drones and autonomous vehicles were introduced into new uses. Nuclear plants, deep underwater and space vehicles are some of the areas computer vision can be applied to develop a fully autonomous system. Furthermore, the development … full description “Computer Vision for Extreme Environments (available)”

Coq Formalisation of Recursive Adaptive Grammars (available)

The aim of this project is to formalise within the Coq proof assistant [1] the meta-theory of the recursive adaptive grammar framework [2] Programming languages are usually specified on two levels. The first level defines a context-free grammar that specifies the syntax of the language. Usually, however, not all syntactically correct programs make sense, and … full description “Coq Formalisation of Recursive Adaptive Grammars (available)”

Corporate Transparency – Enabling Consumers Track and Vet their Data Usage (available)

Project Description Data, primarily related to consumers is a crucial part of the modern tech-companies like Google, Facebook, Instagram, and non-tech-companies (superstores, insurance companies, etc.) alike have now started to rely heavily on consumer data for various commercial activities. Although the General Data Protection Regulation (GDPR) enhances the rights of the consumers from a technical … full description “Corporate Transparency – Enabling Consumers Track and Vet their Data Usage (available)”

Correct and Certified Regular Expressions (available)

In programming language research ideas are explored in an ofte repeated loop. You have an idea then propose the language feature to study, its semantics, and the prove it has the properties you expect (type safety, performance, expressivity, etc.). In this project, we want to explore such a cycle working with regular expressions as the … full description “Correct and Certified Regular Expressions (available)”

COVID-19 – Mobile phone based passport applications (available)

Project Description We have all been affected by COVID19. Amongst the main driving forces for reopening international borders and enabling traveling is the existence of COVID19 immunity passports. However, there are serious considerations around the overall trust, security, privacy but also ethical dimensions of such proposals. This project aims to take into account the views … full description “COVID-19 – Mobile phone based passport applications (available)”

Cyclist: Verifying Programs using Cyclic Proof (available)

Cyclic proofs are a technique for proving properties inductively, or proving properties about inductively defined objects or processes. They can be used to prove logical statements, or to verify recursive programs. The Cyclist tool [1] has been developed as an automatic verification tool based on cyclic proofs. It can prove termination and verify temporal properties … full description “Cyclist: Verifying Programs using Cyclic Proof (available)”

Deep learning based underwater image enhancement and object recognition (available)

In the past decade, advances in marine object recognition have been dramatically boosted for monitoring of underwater ecosystems. Traditional statistical analysis and ocean model simulation heavily depend on the availability of visual features. However, Due to light attenuation and scattering problem, the underwater images captured by optical imaging system are heavily degraded. As a result, … full description “Deep learning based underwater image enhancement and object recognition (available)”

Deep Learning-based Environmental Sound Classification (available)

Automatic sound classification attracts increasing research attention owing to its vast applications, such as robot navigation, environmental sensing, musical instrument classification, medical diagnosis, and surveillance. Sound classification tasks involve the extraction of acoustic characteristics from the audio signals and the subsequent identification of different sound classes. The broad range of sound classification deployments can be … full description “Deep Learning-based Environmental Sound Classification (available)”

Detecting money laundering in cryptocurrency economy (available)

Project Description Cryptocurrency networks are unique in a way that all the transactions are public. All payers and receivers are known, and their respective pseudonyms are public. Whereas the inherent anonymity enabled by the pseudonyms and privacy-preserving protocols, cryptocurrency can be argued to be a suitable platform for money laundering activities. In this project, the … full description “Detecting money laundering in cryptocurrency economy (available)”

Digital Humans in a Virtual Reality Football Platform. (available)

Libero is a VR football platform; a ground-breaking experience in visitor focused, immersive content that allows fans to truly live the history of famous football clubs, whilst also giving them a glimpse of what the future holds. Using A.I., world-class animation and award-winning storytelling, we can engage fans, new and old, in a way that … full description “Digital Humans in a Virtual Reality Football Platform. (available)”

Federated Machine Learning – Security and Privacy Evaluation Framework (available)

Project Description User data is essential for many of the modern business operations, especially related to the building consumer segmentation and profiling – for marketing and services personalisation. Dealing with user data has its positive and negatives, especially after the General Data Protection Regulation (GDPR) collecting and storing user’s personal data. Centralised machine learning approaches … full description “Federated Machine Learning – Security and Privacy Evaluation Framework (available)”

Increasing the Efficiency of Low-land Natural Disaster Search and Rescue through ‘Supervised Hybrid Animal-UAV Interactions’ (available)

Search and Rescue (SAR) is a time-critical event: after a finite period of time the chances of recovering individuals who have become lost, or trapped in the wake of a disaster, trend towards zero. As a result, management of search and rescue resources is paramount. Travel time, planning and executing search grids, are pivotal tasks … full description “Increasing the Efficiency of Low-land Natural Disaster Search and Rescue through ‘Supervised Hybrid Animal-UAV Interactions’ (available)”

Jupyter notebooks (available)

  Prerequisites: experience with Python (useful) and Javascriptprogramming (essential). It may be useful to be willing to learn aboutfunctional programming (but this is not essential). Jupyter notebooks [1] are examples of literate programming [2] wherecode and outputs from the code as well as documentation are in the sameapplication. Jupyter allows the user to run code … full description “Jupyter notebooks (available)”

Machine Learning for Cyber-Physical Systems Monitoring (available)

Hybrid automata (HA) are a formal model for cyber-physical systems, i.e., systems characterised by digital components (discrete) that control and interact with the physical environment (continuous). HAs have been applied to system designs in numerous domains including avionics, automotive, medical devices, and robotics. Formal verification of HAs can establish, with provable correctness guarantees, whether or … full description “Machine Learning for Cyber-Physical Systems Monitoring (available)”

Maritime Cybersecurity (available)

Project Description Connected objects in motion are developing as a significant domain. There are many traditional businesses, like logistics and maritime shipping that have legacy systems, but they are rolling out interconnectivity globally. Today’s shift towards increasing interconnectedness at sea is continuing to enable significant efficiency gains and new capabilities for maritime operations. Running in … full description “Maritime Cybersecurity (available)”

Mechanisation of subtyping for Go 1.18 (available)

Go 1.18 [1] has recently been released. This new version includes generics and more flexible interfaces. Generics allow programmers to define data structures and functions that work safely for several types, e.g., like List<E> in Java which defines lists that can store any value of type E, where E is any type (String, Boolean, etc). … full description “Mechanisation of subtyping for Go 1.18 (available)”