DTC CS 1 - Project Title: Verification of Bitcoins and other Cryptocurrencies.

Project Description:

This project would connect well with research by Pedro Helles in the School of Law on smart contracts and cryptocurrencies. While there has been a lot of interest in the media in Bitcoins, with the price for Bitcoins increasing from 1003 US-$ on 1/1/2017 to 8155 US-$ at time of writing, there exist no formal proof yet  that the protocol is actually correct, which is worrying, since Bitcoins rely entirely on the algorithm with no human organisation mediating it. The goal of this project is to fix this gap and to formally verify the Bitcoin protocol and protocols of other cryptocurrencies in the interactive theorem proving tool Agda.


DTC CS 2 - Project Title: Development of a language for writing smart contracts.

Project Description:

This project would connect well with research by Pedro Helles in the School of Law on smart contracts and cryptocurrencies. Smart contracts allow to formalise contractual relationships regarding exchange of money using cryptocurrencies in a purely algorithmic way without any involvement of legal entities, but can lead to loss of money as in the DAO attack on Ethereum, where the loss of 100 Million US-$ was only avoided by creating a hard fork, violating the principle that cryptocurrencies are entirely governed by algorithms. The goal of this project is to develop based on the interactive theorem prover Agda a language for smart contracts, in which correctness proofs can be carried out, and therefore contractors can rely on the correctness of their contracts.


DTC CS 3 - Project Title: Beyond sigma-frames

Project Description:

Formal topology is the notion of a frame studied as an abstraction of the collection of open subsets of a topological space. While the opens of a frame are closed under arbitrary unions and finite intersections, this is related to closure under countable unions and finite intersection to obtain the notion of a sigma-frame. In this project, variations of frames with specific closure properties will be studied in order to make formal topology applicable to descriptive set theory.


 DTC CS 4 - Project Title: Computational complexity and bounded rationality

Project Description:

If figuring out the best way to play a game is too complicated to be feasible, what is the next best approach? This project combines computational complexity and algorithmic game theory to search for a notion of rational behaviour under complexity constraints. This is a step towards bridging the gap between mathematical theory and experimental observations in game theory.


DTC CS 5 - Project Title: Deep Learning on Irregular Domains

Project Description:

The Swansea Vision group (csvision.swan.ac.uk) is one of the first to introduce Deep Neural Network based Machine Learning to domains and spaces where their structures are defined as regular grids, e.g. images. This project aims to both advance its fundamental techniques and demonstrate its effectiveness in various real-world applications, e.g. social network analysis, medicine, biology, and computer vision.


DTC CS 6 - Project Title: Data Mining and Predictive Data Analytics 

Project Description:

The Swansea Vision group (csvision.swan.ac.uk) has been working very closely with collaborator in health and social sciences. This project aims to develop robust and efficient analytical predictive tools using advanced data mining and machine learning. The student will join a team of researchers with extensive experience in deep learning and data mining and work closely with our collaborators, such as Swansea Health Data Science and Cardiff University Brain Imaging Research Centre.


 DTC CS 7 - Project Title: Non-Rigid Surface Registration and Deep Learning On Facial Dynamics

Project Description:

Analysis of 4D facial dynamics is a fundamental problem in computer graphics and vision, having far-reaching applications in many areas like movie production, animation, game development, medical imaging, psychology and facial expression recognition, dental surgery, virtual and augmented reality, architectural (CAD) design, and even advertising industry. It is one of the strongest growing areas in the Creative Economy in the UK. This project will investigate various constraints and deep learning models to assist the development of robust non-rigid surface registration techniques, for the analysis of 4D facial dynamics. You will need to demonstrate good mathematics and programming skills.


 DTC CS 8 - Project Title: Visual Analytics of Financial Time Series

Project Description:

Financial data analysis is a challenging problem in financial market research (e.g. stock market prediction) as it depends not only on supply-and-demand but also changing market conditions. This project will investigate visual analytics, interactive pattern matching techniques and machine learning to support the understanding of the financial market – a growing area in Creative Economy in the UK. Your good mathematics and programming skills will drive the project in trend forecasting, traders experience capturing, the development of user decision models, comprehension of trading decisions, and therefore responsible trading.


DTC CS 9 - Project Title: Algorithms for very hard satisfiability problems (SAT)

Project Description:

The article "The Science of Brute Force",
Communications of the ACM, Vol. 60 No. 8, gives an overview of exciting new developments in the area of solving hard computational problems, via SAT solving. The PhD can be about the theory, implementations, applications, or any combination thereof, of algorithms and the underlying problem structures, focussing on hard SAT problems.


DTC CS 10 - Project Title: Combinatorics of Satisfiability

Project Description:

Solving boolean systems of equations (the SAT problem) and combinatorics have deep connections, and a theory of SAT is emerging. This PhD will be about strengthening these connections, developing new synergies with mathematics, combinatorics, complexity theory and algorithmics.


 DTC CS 12 - Project Title: AI-assisted big astrophysics data analysis

Project Description:

This project aims at leveraging and further developing the state-of-the-art in computer vision and machine learning to assist in the analysis of the large quantity of observational data gathered in astrophysics research. It is a computer science project, in collaboration with astrophysics experts who will be the end-users of the developed data analysis methods and tools. The PhD student will get to use methods such as deep learning, multispectral image analysis, and machine learning based predictions.


DTC CS 13 - Project Title: Fast DNA alignment algorithms for mainstream DNA analysis

Project Description:

Alignment of DNA sequences has had a profound impact on health science – e.g. cancer genome sequencing for targeted therapy or identification of genetic disorders –  but is still unfortunately very costly due to the huge amount of processing power needed. This is mainly due to the complexity of the alignment algorithms used for solving the problem.

The Fellowship will offer the opportunity to work on a new family of algorithms that are several orders of magnitude faster than current technologies and allow DNA analysis to become mainstream in the health sector as well as in other sciences.


DTC CS 14 - Project Title: Improving 3D printing technologies

Project Description:

The 3D printing revolution has changed the way we prototype models by accelerating and simplifying design. There are however algorithmically challenging aspects of 3D printers that still need to be researched about. This fellowship will work on new algorithms for 3D printing in the area of ray-traced model visualisation, mesh generation, and head-travel path optimisations.


DTC CS 15 - Project Title: Computing with Infinite Data

Project Description:

Infinite or virtually infinite data occur naturally when processing very large data sets or exact real numbers, and computing with such data poses many theoretical and practical challenges.  Computing with Infinite Data (CID,http://cordis.europa.eu/project/rcn/207017_en.html, http://www.cs.swansea.ac.uk/theory/index.php/cid/) is a four-year Horizon 2020 project, starting in April 2017, that will provide the opportunity and means for two PhD students to spend several months abroad in order to facilitate research and knowledge exchange in that area.  The proposed research will focus on logical methods for the specification and extraction of formally verified algorithms for infinite data.


DTC CS 16 - Project Title: Big Data Visualization

Project Description:

We are looking for PhD candidates interested in developing novel methods for visualization of large, multivariate, time-dependent data sets.  Topics include information visualization, scientific visualization, and visual analytics.  Please contact me if you are interested and we can discuss topics in more detail.


DTC CS 17 - Project Title: Smart speakers in emergent user communities

Project Description:

Speech and conversational interfaces are becoming increasingly popular in homes and workplaces in developed countries. For emergent users - those with typically low literacy, disposable income and access to education and technology - such systems currently seem a long way off. There are many potential benefits of these systems in such contexts, however, whether in public or private settings, or in a variety of physical forms: this project will explore the possibilities for smart speakers with emergent users.


DTC CS 18 - Project Title: Sustainable self-powered interfaces

Project Description:

As the digital future and the Internet of Things spreads ever more into our everyday lives, there is an increasing drive for the technologies in these visions to be sustainable and energy efficient. In collaboration with materials scientists, this project will explore the potential for future IoT devices that are sustainably powered, but still able to provide practical and pleasing interactive experiences.


DTC CS 19 - Project Title: Formal Models for Cyber Security Analysis

Project Description:

Traditionally, formal methods have been used to analyse security protocols. This project will consider modelling various security vulnerabilities/attacks and using these to analyse the best form of defence against such attacks. A starting point may be to consider work into the use of game theoretic approaches.


DTC CS 20 - Project Title: Traceability of Security Requirements in Model-Based Software

Project Description:

Model-based software engineering is often based upon the notion of a model transformation. This project will explore how security requirements can be "traced" through such transformations. This may involve extensions of exiting transformation frameworks or development of a new one.


DTC CS 21 - Project Title: Extracting advanced SMT solvers from proofs

First Supervisor Name: Dr Monika Seisenberger, m.seisenberger@swansea.ac.uk
Link to Staff Profile: http://www.swansea.ac.uk/staff/science/computer-science/m.seisenberger/

Project Description:

In U. Berger, A. Lawrence. F. Nordvall Forsberg, M. Seisenberger, Extracting Verified Decisions Procedures, LMCS, 2015, it was demonstrated how to extract a basic SAT solver from a proof. The objective of this PhD project is to lift this technique to the next level and extract SMT solvers, i.e. solvers that can deal with a much richer logical language, and therefore cover many more problems. In particular we have problems in mind arising from the industrial context (connection to Railway Verification), and conversely, on the theoretical side, also want to be able to deal with infinite clauses sets (connection to the Computing with Infinite Data (CID) project), and more advanced problems arising in Complexity theory.

How to apply for a Computer Science Research Degree Project

Details can be found in the ‘How to Apply’ section on our PhD course page: https://www.swansea.ac.uk/postgraduate/research/science/computer-science/phd-mphil-msc-by-research-computer-science/