Current Research Projects

Examples of projects on which CDT in Pervasive Parallelism supervisors and students are currently working.

A Basis for Concurrency and Distribution (ABCD): From Data Types to Session Types

Concurrency and distribution are computing’s most pressing problem. The data type is one of computing’s most successful ideas. Session types codify the structure of communication, making software more reliable and easier to construct, and will therefore play a crucial role in all aspects of software.

Application stores are set to become the dominant model for software distribution. App Guarden’s research examines a number of improvements to app stores and mobile device operating systems which will take us closer to future generation, secure app stores.

ThreadSafe: Static Analysis for Java Concurrency

Issues around concurrency and multithreading are the worst bugs software can have. They tend to be intermittent and so can only be detected by chance during testing. The effect of such defects can be disastrous: deadlocks can result in the system hanging, race conditions can drastically alter important data values without reporting any error. Threadsafe, a product of Contemplate Ltd, is a static analysis tool for finding and diagnosing dangerous concurrency bugs in Java code, and is based on cutting-edge academic research.

Collaborative Research into Exascale Systemware, Tools and Applications (CRESTA)

Developing techniques and solutions which address the most difficult challenges that computing at the exascale can provide. The supercomputing community worldwide has set itself the challenge of delivering an exaflop (or a million million million calculations per second) by the end of this decade. CRESTA is committed to ensuring Europe is at the forefront of solving this worldwide challenge.

Mobility and Security Group, Laboratory for Foundations of Computer Science

We have a range of projects and collaborations in the area of programming language security for systems which depend on the mobility of code, data, or both. Common themes include ensuring the secure use of resources such as time, memory space, or network access; and the verification of security with machine-checked proof.

Processor Automated Synthesis by iTerative Analysis Project (PASTA)

In the PASTA project we seek to automate the design and optimisation of customisable embedded processors. We do this by creating tools that are able to learn about the physical characteristics of the underlying silicon technology, and use that knowledge to synthesise the structure of an embedded processor.

A Predictive Modelling based Approach to Portable Parallel Compilation for Heterogeneous Multi-cores (PreMapp)

This project aims to prevent software stagnation by investigating new techniques to automatically learn how to utilise new multi-core platforms. Using ideas and techniques first developed in artificial intelligence, we will develop a system that automatically learns how to adapt software to work on new platforms.

 A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours (QUANTICOL)

The main objective of the QUANTICOL project is the development of an innovative formal design framework that provides a specification language for collective adaptive systems (CAS) and a large variety of tool-supported, scalable analysis and verification techniques. These techniques are based on stochastic process algebras and associated verification techniques, and mean field/continuous approximation and control theory. This design framework will provide scalable extensive support for the verification of developed models, and also enable and facilitate experimentation and discovery of new design patterns for emergent behaviour and control over spatially distributed CAS.

REMS: Rigorous Engineering for Mainstream Systems

How can we use rigorous maths to improve the quality of mainstream computer systems? REMS is a 6-year EPSRC-funded Programme Grant to do just that, bringing together an exciting combination of researchers in systems (architecture, operating systems, and networks) and in semantics (programming languages, automated reasoning, and verification) at Cambridge, Imperial, and Edinburgh.