School of Engineering and Informatics (for staff and students)

Example Projects

Example projects from the 2016 Junior Research Associates Scheme:

 

Higher-kinded Types

Project Supervisor: Martin Berger

Types are one of the key contributions of theoretical computer science to modern software engineering. Types offer a lightweight and exhaustive check for simple sequential program properties. For example, types can detect faulty programs like

3 * "hello"

This program is defective because strings cannot be multiplied -- multiplication is defined only on numbers. Type-checking finds such problems even in extremely large code bases, leading to lower software development costs. The basic theory of such types is now mature, and the last few years have seen substantial industrial uptake of languages with modern approaches to typing (e.g. Scala, C#, F#, Swift, Rust, Facebook's Flow, a static type checker for JavaScript).

However, types as currently used in practice have two glaring and orthogonal shortcomings.

  • Simplicity barrier. Types work well only for avoiding simple errors, e.g. one cannot use types in mainstream programming languages to specify that a program should sort an array.
  • Sequentiality barrier. Types prevent errors only for sequential computation, i.e. they do not prevent errors arising from parallel computation.

Both barriers are under active but separate investigation.

Research on overcoming the simplicity barrier led to higher-kinded types. They are used in Haskell and Scala. Research on overcoming the sequentiality barrier is also picking up steam, particularly with interaction types (such as e.g. session types). What is lacking at this point is a connection between those distinct research efforts. In other words, we currently don't have types that can enforce rich properties of parallel computation.

The FOSS (Foundations of Software Systems) group is currently investigating how to improve this situation, starting from a theoretical angle. It would be nice to complement this work with implementations. The JRA project is about implementing a compiler for a modern programming language with higher-kinded types. This language and compiler would then serve as a vehicle for further research on higher-kinded interaction types.

This project will suit a student with an interest in programming languages and compilers. Good programming skills and knowledge of compilers essential. Previous experience with advanced typing systems and type inference would be ideal.

Reliability of DPLL Implementations

Project Supervisor: Martin Berger

Satisfiability (SAT) is the problem of deciding whether a formula in propositional logic has a solution or not. For example the formula

( x or y or not z ) and ( a or not x )

has a solution y = true and x = false. In contrast the formula

y and not y

has no solution. Despite the deceptive simplicity of the SAT, it is one of the most famous algorithmic problems in CS, for two reasons

  • It is widely used in practise (e.g. cryptography, motion planning in robotics, verification of programs and CPU chips, scheduling of air-planes, ... and many more). SAT has been called the "assembly language of optimisation problems".
  • It seems algorithmically hard. All known algorithms run in worst-case O(2^n) time, where n is the number of variables in the formula. However, nobody has been able to prove that such a terrible worst-case complexity is necessary. Maybe a faster algorithm exists, waiting to be discovered? The theoretical study of algorithms for SAT lead to the P=NP? question, the most famous open problem in computer science, and one of the most famous open questions in science.

All the existing algorithms are refinements of a naive algorithm called DPLL (initials of the inventors). It is known from theoretical investigations, that DPLL is not a good algorithm: it has exponential worst-case complexity. Despite not working in theory, it refinements of DPLL work extremely well in practise on SAT instances that arise in industrial applications. It is not understood why.

These theoretical questions aside, modern implementations of DPLL are rather complicated. How do we know that they are actually correct?

The purpose of the JRA project is to investigate the correctness of DPLL implementations. To achieve maximal reliability, DPLL should be implemented using an interactive proof assistant (e.g. Isabelle/HOL or Coq) and the prove the correctness of the implementation.

The FOSS (Foundations of Software Systems) group has been working on tools and methods for correct software for a long time, so the project fits very well with the group's research agenda. The result of the JRA would then serve as a vehicle for further research on program correctness.

This project will suit a student with an interest in programming languages, logic and algorithms. Good programming skills essential.

Evolving Networks that Satisfy Contraints

Project Supervisor: Luc Berthouze

Real-world networks such as large-scale computer networks or social networks are often described in terms of some global structural property (e.g., scale-free) but this overlooks higher-order structure provided by the presence of motifs (e.g., fully-connected squares) in the network. As motifs are recognised as playing an important role in the behaviour of the system, there is a need to understand how diverse networks that satisfy a particular set of constraints can be. In this project, you will contribute to the development of a GA-based framework for mapping out the space of network solutions given a set of constraints. An important codebase will be made available and you will be working tightly with the group.

Good knowledge of Python and/or MATLAB is essential. Interest in distributed computing is desirable.

Semantic Similarity and Neural Representation

Project Supervisor: Bill Keller

Functional MRI (fMRI) is a technique used to measure brain activity. fMRI studies at Sussex aim to identify where in the brain conceptual/semantic knowledge is represented. Study participants look at pictures of objects whilst being scanned. Regions are then identified where brain activity is similar whenever similar objects are presented.

To better identify regions of semantic representation it is proposed to quantify semantic similarity of stimuli. This project would involve exploring techniques from language processing to assign numerical scores representing proximity in semantic space: e.g. “apple” versus “broccoli” or “zebra” versus “hammer”. These associations can then be compared to patterns observed in the brain.

The WOW Experience: An EEG investigation of Awesome Engineering

Project Supervisor: Marianna Obrist

The world surrounding us is filled with moments able to take our breath away, leaving us in a state of awe. This project aims to, for the first time, investigate the feeling of wonder (awe) in relation with human artefacts. This involves using Electroencephalography (EEG) to identify characteristic patterns in brain activity during the presentation of awesome stimuli. The findings will help to theorize the importance of understanding causality and the fulfilling of expectation that might play an important role in such cognitive phenomenon. The project would particularly suit students who have some basic understanding in running user studies, and signal processing (to analyse EEG data). See details about the SCHI Lab research and team you would work with: http://multi-sensory.info/

Multisensory Emotions: What Emotions Technology can mediate

Project Supervisor: Marianna Obrist

The aim of this project is to help in understanding the relationship between different sensory modalities in their ability to communicate and express emotions. Every day’s life is full of examples highlighting these connections. Sound, touch, smell, taste, and vision all play a role in our emotional experiences. So far, this connection between senses and emotions has never been explored from a computational perspective. In this project we approach the problem in the Bayesian framework. Results may support us in designing new user interfaces for different contexts and purposes. The project would particularly suit students who have some basic understanding in running user studies, and are interested in HCI and interaction design. See details about the SCHI Lab research and team you would work with: http://multi-sensory.info/

Geo-casting in Opportunistic Networks

Project Supervisor: George Parisis

Second Supervisor: Ian Wakeman

In opportunistic wireless networks, communication among network nodes is intermittent, so an end-to-end path between the source and the destination may never exist. Mobile nodes have no information about the network topology which constantly changes. Routes are built

dynamically, while messages are en route between the sender and the destination(s), and any possible node can opportunistically be used as next hop, provided it is likely to bring the message closer to the final destination. Routing is based on the store-carry-forward approach where a mobile device physically carries a message towards its destination exploiting node mobility which is inherent in opportunistic networks.

In the FoSS research group we are researching ways to efficiently route data within opportunistic networks. Currently, we focus on how to route data by using geographical regions as the destination information carried with each message (geo-casting). This is very different to routing data to explicitly specified nodes or sets of nodes (e.g. through the usage of unicast or multicast addresses). This JRA is about extending our existing approaches [1] (mainly to improve the delivery ratio and message delivery latency) to geo-casting in the ONE [2] network simulator which is written in Java.

[1] A. Rajaey, D. Chalmers, I. Wakeman and G. Parisis, "GSAF: Efficient and Flexible Geocasting for Opportunistic Networks", In IEEE WoWMoM 2016, Coimbra, Portugal.

[2] The ONE Simulator, https://akeranen.github.io/the-one/

Simulating Crowd Mobility and Evacuation Scenarios

Project Supervisor: George Parisis

Second Supervisor: Ian Wakeman

In the FoSS research group we are looking at how to provide localisation services to mobile devices in the absence of network infra-structure, such as 3G/4G and WiFi, and location services, such as GPS. We are also looking at how information can be efficiently routed in infrastructure-less, opportunistically created mobile networks exploiting location information that each mobile device maintains and updates. Recipients of information may be specific mobile devices, groups of devices or specific locations. Our research is applicable to emergency management and evacuation scenarios (e.g. after natural disasters, accidents or terrorist attacks), when people must evacuate (small or even large areas) while the network infrastructure is not accessible (or is damaged). Information needs to be exchanged from emergency services to people’s devices (or vice versa) but also among people’s devices.

This JRA is about implementing crowd mobility and evacuation models [1] in the widely used ONE [2] simulator. ONE is a Java-based simulation environment for generating node movement using different movement models, routing messages between nodes as well as visualising mobility and message passing in real time in its graphical user interface.

[1] Crowd Simulation, http://crowdsimulation.blogspot.co.uk/

[2] The ONE Simulator, https://akeranen.github.io/the-one/

Medical Data Analysis Tools

Project Supervisor: Bernhard Reus

Immunology researchers in the Medical School (BSMS) work with large datasets of anonymised patient data. Based on a mySQL table with over 3.2 million records of blood measurements, we are currently carrying out some analysis of this data. 

The aim is to find any type of correlation yet unknown to the immunologist. The dependencies could be, for instance, between different abnormal measurements of patients or between labs.  

A large amount of work has already been undertaken to clean and prepare this data. For this project, the JRA would be writing some interfaces that support the outlined analysis. This will involve SQL programming, and implementing intuitive (web-based) graphical user interfaces for medical staff. It may also involve looking into automatic statistical and machine learning methods to discover patterns in the data.

The candidate must be a strong programmer (must be fluent in SQL and standard web technology), but should also have some interest in statistics and machine learning. The candidate does not need to have any medical knowledge.

Stronger Types - Better Types - Dependent Types

Project Supervisor: Bernhard Reus

Dependent types do not only depend on other types like polymorphic types do, (e.g. Generics in Java) but also on values. For instance, List<Int> denotes the polymorphic type of lists containing integers, but the length of the lists is unrestricted. A dependent type List<Int,n> describes lists of integers of length n. By making assumptions about n, one can, for instance, stipulate that the list must not be empty, or that the input to a zip function are two lists of the same length. The stronger typing discipline allows for catching more programming errors and thus more reliable software.

Agda [1] is a language for scalable dependently typed programming, strongly influenced by other experimental languages like Cayenne and Epigram.  This project is supposed to introduce an interested student to the exciting world of dependently typed programming. 

The JRA would learn Agda, starting with simple examples, grasping the concepts and applications of dependently typed programs. Ideally, at the end, the JRA would implement a type theoretical language in Agda itself. 

This project is ideal for someone who is interested in a MSc or PhD in this area later.

[1] Agda: http://wiki.portal.chalmers.se/agda

Distributed Database Technology

Project Supervisor: Bernhard Reus

In the context of what is often called “big data”, new database technologies have emerged that differ significantly from the classic relational database. For large popular websites scaling becomes an issue, requiring more than one server and enforcing data to be fragmented accordingly (vertically or horizontally, i.e. by column or by row).

This project is about exploring the world of distributed (noSQL) databases and investigating one or two particular systems, for instance HBase [1]. The project would require the installation of such systems, the setup of some reasonably sized examples, and an evaluation of the advantages and disadvantages encountered in the process. Good results may be re-used in our Database 2nd year module.

The JRA must have a very good understanding of SQL databases, be handy with software installations, and be courageous enough to explore new technologies, a trait that would be essential for a MSc or PhD later.

[1] HBase https://hbase.apache.org/

School of Engineering and Informatics (for staff and students)

School Office:
School of Engineering and Informatics, University of Sussex, Chichester 1 Room 002, Falmer, Brighton, BN1 9QJ
enquiries@enginf.sussex.ac.uk
T 01273 (67) 8195

School Office opening hours: Monday - Friday 09.00 - 17.00
School Office location [PDF 1.74MB]