Previous Projects : Junior Research Associates : ... : School of Engineering and Informatics : Schools and services : ��Ƶ

Previous Projects

Example projects from previous Junior Research Associates Schemes:

2023

NLP Meets Temporal Logics

Supervisor:

Recently there have been some attempts to apply modern NLP / machine learning techniques to traditional logical/mathematical reasoning tasks, e.g., simple arithmetic or Boolean formula satisfiabilty. A recent work, which applies the Transformer architecture to the problem of finding solutions to temporal logic formulas, which has many applications in e.g., control engineering and robotic motion planning. https://openreview.net/forum?id=dOcQK-f4byz

The goal of the project is to advance the state of the art by applying similar techniques to more expressive temporal logics (e.g., with timing constraints). It is likely that the result will degrade as the formulas will be more complicated, thus it is also expected that one needs some novel ideas to improve the performance.

Developing Efficient Network Protocols for Low-Earth Orbit Satellite Networks

Supervisor:

Thousands of Low Earth Orbit (LEO) satellites currently orbit the Earth, which are major components of vast constellations with the goal of 100% geographic coverage. Various private companies (e.g., SpaceX, OneWeb) currently lead the race with billion-dollar investments in place [1]. These constellations exhibit a unique combination of characteristics [2, 3, 4]; (1) aggregate bandwidth in the order of hundreds of Tbps, which is comparble to today's aggregate bre capacity [2]; (2) multiple paths in a dense and constantly changing network topology; (3) sub-10ms round-trip time between the Earth and the rst-hop satellite; (4) low but varying end-to-end latency that can be smaller than what the best theoretical bre path can support. With these characteristics being collectively unprecedented, a major rethink of routing and data transport mechanisms are needed to ensure ecient usage of network resources.

This JRA project is part of a broader research eort in devising next generation data transport for LEO satellite constellations. The project will involve using a LEO satellite constellation simulation model [5], written in C++ using the OMNeT++ framework [6], developed internally by the Packets Lab.

References:
[1] Tobias Klenze, Giacomo Giuliari, Christos Pappas, Adrian Perrig, and David Basin. Networking in Heaven as on Earth. In Proceedings of the
17th ACM Workshop on Hot Topics in Networks, pages 22{28, Redmond WA USA, November 2018. ACM.

[2] Debopam Bhattacherjee, Waqar Aqeel, Ilker Nadi Bozkurt, Anthony Aguirre, Balakrishnan Chandrasekaran, P. Brighten Godfrey, Gregory
Laughlin, Bruce Maggs, and Ankit Singla. Gearing up for the 21st century space race. In Proceedings of the 17th ACM Workshop on Hot Topics in Networks, pages 113{119, Redmond WA USA, November 2018. ACM.

[3] Mark Handley. Delay is Not an Option: Low Latency Routing in Space. In Proceedings of the 17th ACM Workshop on Hot Topics in Networks,
pages 85{91, Redmond WA USA, November 2018. ACM.

[4] Mark Handley. Using ground relays for low-latency wide-area routing in megaconstellations. In Proceedings of the 18th ACM Workshop on Hot
Topics in Networks, HotNets '19, pages 125{132, New York, NY, USA, 2019. Association for Computing Machinery.

[5] Aiden Valentine and George Parisis. Developing and experimenting with LEO satellite constellations in OMNeT++. In Proceedings of the 8th
OMNeT++ Community Summit 2021, September 2021.
[6] OMNeT++. https://omnetpp.org/.

Synthesis for Binary Lambda Calculus

Supervisor:

Binary lambda calculus (BLC) is a succinct encoding of a minimal programming language. Recently it is shown that it can also be implemented on existing architectures (C, x86) with an extraordinarily small footprint: https://justine.lol/lambda/

The goal of the project is to explore the viability of data-intensive approaches for program synthesis, using BLC as a representation. Applications include:

compiler for BLC programs
automated synthesis of BLC programs
minimal implementations in hardware, e.g., crypto

Neuromorphic Animal Tracking New row title

Supervisor: James Knight, Paul Graham

Visual tracking of animals can provide rich data which can enable breakthroughs in biological research. However, few existing methods extend to tracking natural behaviour in the field. Issues include difficulties in maintaining the identity of an individual animal between frames and dealing with complex backgrounds. Neuromorphic vision sensors (https://inivation.com/) have the potential to solve both of these problems and, in this project, the JRA will investigate their suitability for tracking wood ants in natural environments. Specifically, they will work to develop suitable algorithms based on pre-recorded data before, potentially, working with students who are performing experiments in the field, to validate their methods.

Model Checking Properties of Programmable Networks

Supervisor: Dr Bernhard Reus

Software Defined Networking (SDN) is a new paradigm for operating and managing computer networks. SDN allows anyone to write SDN applications but this could potentially result in poorly written and very buggy software. It is therefore crucial to develop techniques for verifying the correctness of software-defined network functionality like absence of black holes or loops. This project investigates whether network properties can be verified with the model checking tool ESBMC. More precisely, using simple examples, investigate: 1) How to best model a SDN network as a concurrent C program? 2) Can ESBMC handle those C programs to verify important safety properties?

[1] L. Cordeiro and B. Fischer. Verifying Multi-Threaded Software using SMT-based Context-Bounded Model Checking. ICSE, pp. 331–340, 2011. https://ieeexplore.ieee.org/document/6032472

[2] Klimis, Vassilis, Parisis, George and Reus, Bernhard: Towards model checking real-world software-defined networks. In: Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science. 12225 126-148. Springer Verlag. http://sro.sussex.ac.uk/id/eprint/90723/5/Klimis2020_Chapter_TowardsModelCheckingReal-World.pdf

[3] ESBMC online manual: https://ssvlab.github.io/esbmc/documentation.html

2022

Distributed graph processing in the Kuramoto model of synchronisation

Project Supervisor:

The Kuramoto model [1] is often used to study synchronisation in the brain. In its simplest form, the model assumes a fully connected network, but it can be adapted to operate on more realistic networks. We are interested in understanding how network structure impacts synchronisation. This involves running a large number of simulations using different network structures. For large networks, this is computationally intensive. The goal of this JRA project is to explore the use of a distributed graph processing platform [2] such as Giraph to accelerate this process. Strong experience coding in Java and interest in distributed processing is essential.

[1] See: http://tutorials.siam.org/dsweb/cotutorial/for an easy introduction. For more detail, see Acebrón et al. (2005). The Kuramoto model: A simple paradigm for synchronization phenomena. Reviews of modern physics. 77(1):137. Available at: https://www.researchgate.net/publication/46776356_The_Kuramoto_model_A_simple_paradigm_for_synchronization_phenomena.

[2] Malewicz et al. (2010). Pregel: a system for large-scale graph processing. In Proceedings of the 2010 ACM SIGMOD International Conference on Management of data (pp. 135-146). Available at: https://www.cs.cmu.edu/~pavlo/courses/fall2013/static/papers/p135-malewicz.pdf

NLP meets temporal logics

Project Supervisor:

https://openreview.net/forum?id=dOcQK-f4byz

The goal of theproject is to advance the state of the art by applying similar techniques to more expressive temporal logics (e.g., with timing constraints). It is likely that the result will degrade as the formulas will be more complicated, thus it is also expected thatone needs some novel ideas to improve the performance.

Document layout analysis for exam scripts

Project Supervisor:

Document image analysis (DIA) plays a key role in modern social sciences and humanities research. While there have been many success stories in various individual projects based on recent advances in using deep learning for DIA, many of these required specialised training or post-processing steps to achieve satisfactory performances. The goal is to make use of a recently proposed uniform framework for DIA [1] to develop a semi-automated workflow for exam marking -based on the assumption that scanned PDF exam scripts have rather restricted (and known) possible layouts.

[1] Shen et al. LayoutParser: A Unified Toolkit for Deep Learning Based Document Image Analysis. https://arxiv.org/pdf/2103.15348.pdf

Evaluating cryptographic algorithms for secure content dissemination schemes in the Internet of Vehicles

Project Supervisor:

Security is a key challenge on the Internet of Vehicles (IoV) since, nowadays, many security attacks exist that can negatively impact its reliability [1]. Some examples of common threats to vehicles in IoV include denial of service, jamming, the man in the middle, Sybil, eavesdropping, and broadcast and message tampering.

The volume of data required by connected vehicles in IoV will continue to rise, and some of the appealing vehicle content dissemination applications are of upmost importance for the correct functioning of vehicles [2].

This project aims to evaluate novel cryptographic algorithms used for secure content dissemination to avoid attackers from tampering with critical data that would endanger vehicles’ passengers on the Internet of Vehicles.

[1] C. Bernardini, M. R. Asghar, and B. Crispo, “Security and privacy in vehicular communications: Challenges and opportunities,” Vehicular Communications, vol. 10. pp. 13–28, 2017.

[2] N. Magaia, Z. Sheng, P. R. Pereira, and M. Correia, “REPSYS: A robust and distributed incentive scheme for in-network caching and dissemination in Vehicular Delay-Tolerant Networks,” IEEE Wirel. Commun. Mag., pp. 1–16, 2018.

Model Checking Properties of Programmable Networks

Main supervisor:

[1] L. Cordeiro and B. Fischer. Verifying Multi-Threaded Software using SMT-based Context-Bounded Model Checking. ICSE, pp. 331–340, 2011. https://ieeexplore.ieee.org/document/6032472

[3] ESBMC online manual: https://ssvlab.github.io/esbmc/documentation.html

Software to Support the Understanding of HLA-type-associated Disease Risk

Project Supervisor: Dr. Bernhard Reus

Genetically encoded HLA-molecules present ‘self’ and 'foreign' peptides to T-lymphocytes, an important immune cell subset. This may result in protective but also self-destructive (auto)immunity. Therefore, the concrete HLA allele (i.e. gene variation) of a patient may impact their susceptibility to infection and severity of symptoms.

You will support an interdisciplinary research team of computer scientists and immunologists developing a software tool to find novel, statistically relevant associations between HLA alleles and viral diseases like CMV and COVID-19.You will design or write prototype software components to filter data, visualise data, or compute statistical models, depending on your experience.

[1] S.C.L Gough and M.J Simmonds. The HLA Region and Autoimmune Disease: Associations and Mechanisms of Action. Curr Genomics. 2007 Nov; 8(7): 453–465 (2007). https://www.ncbi.nlm.nih.gov/pmc/articles/PMC2647156/

[2] Yanhui Fan and You-Qiang Song. PyHLA: tests for the association between HLA alleles and diseases. BMC Bioinformatics volume 18, 90 (2017). https://bmcbioinformatics.biomedcentral.com/articles/10.1186/s12859-017-1496-0

[3] Douillard Venceslas et al.: Approaching Genetics Through the MHC Lens: Tools and Methods for HLA Research, Frontiers in Genetics 12, 2021.https://www.frontiersin.org/articles/10.3389/fgene.2021.774916/full[4] Douillard Venceslas et al.: Current HLA Investigations on SARS-CoV-2 and Perspectives, Frontiers in Genetics 12, 2021. https://www.frontiersin.org/articles/10.3389/fgene.2021.774922/full

Learning an interpretable model for editing images

Project Supervisor:

Image to image translation models, such as CycleGAN[1], provide a framework for transforming an image from one domain (e.g. horses) to another (e.g. zebras). These methods have enjoyed substantial success in being applied to various domains, however in general the translation functions are overly flexible and lack inspectability, which can result in undesirable changes.

This project would use an iterative neural renderer [2][3], which creates/edits an image through the application of sequential virtual brush strokes as the translation function, this could be extended to model shape changes through geometric transformations [4]. These interpretable editing techniques provide reasonable limits to the complexity of changes and provide a mechanism for human inspection.

[1] Zhu, Jun-Yan, et al. "Unpaired image-to-image translation using cycle-consistent adversarial networks." Proceedings of the IEEE international conference on computer vision. 2017.

[2] Huang et al., Learning to Paint With Model-based Deep Reinforcement Learning, Proceedings of the IEEE international conference on computer vision. 2019.

[3] Ha, David, and Douglas Eck. "A neural representation of sketch drawings." arXiv preprint arXiv:1704.03477 (2017).

[4] Dorta, Garoe, et al. "The GAN that warped: Semantic attribute editing with unpaired data." Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition. 2020

Modelling heterogeneity and uncertainty in neurodegenerative disease progression

Project Supervisor:

Neurodegenerative diseases, such as Alzhiemer's, are known to have heterogeneous presentation across populations. This can complicate differential diagnosis between various forms of dementia, and predicting how a patient's state may degrade over time.

This project will use a public dataset[1,2] containing neurological biomarkers to build machine learning models, such as [3,4,5], that predict disease state/progression give a set of measurements. You will investigate methods to quantify the uncertainty of predictions and better understand population variability.

[1]https://tadpole.grand-challenge.org/

[2] http://adni.loni.usc.edu/

[3]https://github.com/ucl-pond/pySuStaIn

[4] Kingma, Diederik P., and Max Welling. "Auto-encoding variational bayes." ICLR 2013[5] Vaswani, Ashish, et al. "Attention is all you need." Advances in neural information processing systems. 2017.

Developing Efficient Network Protocols for Low-Earth Orbit Satellite Networks

Project Supervisor:

Thousands of Low Earth Orbit (LEO) satellites currently orbit the Earth,which are major components of vast constellations with the goal of 100%geographic coverage. Various private companies (e.g., SpaceX, OneWeb)currently lead the race with billion-dollar investments in place [1]. Theseconstellations exhibit a unique combination of characteristics [2, 3, 4]; (1)aggregate bandwidth in the order of hundreds of Tbps, which is compara-ble to today’s aggregate fibre capacity [2]; (2) multiple paths in a denseand constantly changing network topology; (3) sub-10ms round-trip timebetween the Earth and the first-hop satellite; (4) low but varying end-to-end latency that can be smaller than what the best theoretical fibre pathcan support. With these characteristics being collectively unprecedented,a major rethink of routing and data transport mechanisms are needed toensure efficient usage of network resources.

This JRA project is part of a broader research effort in devising nextgeneration data transport for LEO satellite constellations. The project willinvolve using a LEO satellite constellation simulation model [5], writtenin C++ using the OMNeT++ framework [6], developed internally by thePackets Lab.

References

[1] Tobias Klenze, Giacomo Giuliari, Christos Pappas, Adrian Perrig, andDavid Basin. Networking in Heaven as on Earth. InProceedings of the17th ACM Workshop on Hot Topics in Networks, pages 22–28, RedmondWA USA, November 2018. ACM.

2] Debopam Bhattacherjee, Waqar Aqeel, Ilker Nadi Bozkurt, AnthonyAguirre, Balakrishnan Chandrasekaran, P. Brighten Godfrey, GregoryLaughlin, Bruce Maggs, and Ankit Singla. Gearing up for the 21st cen-tury space race. InProceedings of the 17th ACM Workshop on Hot Topicsin Networks, pages 113–119, Redmond WA USA, November 2018. ACM.

[3] Mark Handley. Delay is Not an Option: Low Latency Routing in Space.InProceedings of the 17th ACM Workshop on Hot Topics in Networks,pages 85–91, Redmond WA USA, November 2018. ACM.

[4] Mark Handley. Using ground relays for low-latency wide-area routing inmegaconstellations. InProceedings of the 18th ACM Workshop on HotTopics in Networks, HotNets ’19, pages 125–132, New York, NY, USA,2019. Association for Computing Machinery.

[5] Aiden Valentine and George Parisis. Developing and experimenting withLEO satellite constellations in OMNeT++. InProceedings of the 8thOMNeT++ Community Summit 2021, September 2021.

[6] OMNeT++. https://omnetpp.org/.

Conversational AI to support Python Debugging

Project Supervisor:

This project is a collaboration with My Code Kit, an Innovate UK backed SME who are developing Ocobox [1] - an AI learning assistant and Python IDE which encourages novice programmers to experiment and fail with confidence. This project involves prototyping conversational interactions for Ocobox including the Python responses and identifying initial sentiments towards them. It forms part of a wider research programme around the use of natural language interactions to support novice programmers [2, 3].

JRA project work will involve:

Collecting regular Python error messages and common feelings/sentiments towards them. (This could potentially be done by scraping public conversations on Twitter and other online sources such as Stack Overflow/ Reddit).
Modelling conversational responses to Python Error Messages (NLP)
Prototyping conversational AI
Collaborating with software engineers to serve machine learning models in production

[1]

[2] Good, Judith, and Kate Howland. Programming language, natural language? Supporting the diverse computational activities of novice programmers. Journal of Visual Languages & Computing 39 (2017): 78-92.

[3] Howland, K., & Good, J. (2015). Learning to communicate computationally with Flip: A bi-modal programming language for game creation. Computers & Education, 80, 224-240.

2016

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 ��Ƶ 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,

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,

[2] The ONE Simulator,

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:

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

��Ƶ

School of Engineering and Informatics (for staff and students)