Concrete topics for PhD research

Roy Crole

Programming language semantics research makes use of techniques from mathematical logic, category theory and type theory to develop the foundations of programming larnguages with a long term goal of producing new and better programming languages and environments. I am interested in axiomatic, operational, categorical and denotational semantics. One creates mathematical models and methods which inform language design and assist with the development of logical systems for specifying and reasoning about program properties. More specifically this research:

  • aims to increase our general understanding of the theory and fundamentals of programming and computation;
  • aims to underpin and clarify our understanding of existing programming languages and systems, and can be used as a basis for analysis, specification, verification, and testing; and
  • can lead to the development of fundamentally new languages and systems.
  1. Mathematical Models of Variable Binding: In the last decade we have advanced our understanding of the formal notion of variable binding considerably. Presheaf categories have been shown to provide models of standard languages with variable binding, such as (variants of) the lambda calculus, as initial algebras. This is a considerable advancement over older models in which expressions with binders could only be realised as alpha-equivalence classes of elements of initial algebras. The important gain here is the initial algebra gives rise to a clear principle of structural induction. My own work has developed particular kinds of presheaf category models, and a PhD thesis could be based upon the further development of these models and the associated reasoning principles.
  2. Computer Systems for Reasoning About Binding: The Hybrid system was developed in Isabelle HOL. It is a metalogic which can be used to reason about languages with binding. One translates the object language into Hybrid, and then uses Hybrid's reasoning principles (such as induction and coinduction) to prove properties of the language. There are a variety of research avenues to explore, ranging from applications of Hybrid which could involve the testing of Hybrid and its comparison with other systems of reasoning with binders, to the further development of the Hybrid system itself.
  3. The Nominal Lambda Calculus The theory of nominal sets has been developed over the past decade as a very general model of variable binding. There are also various kinds of nominal category that provide generalisations of nominal sets. Recent work has been to develop a nominal lambda calculus and a categorical semantics. There are various ways in which these ideas can be further developed, leading to a PhD thesis.

Roy Crole's homepage and contact details


Rayna Dimitrova

Autonomous systems, such as UAVs and self-driving cars, have the potential to bring great benefits to society. The major challenge to the wide adoption of autonomous technology is guaranteeing its safety. Since such systems are often expected to operate in unfamiliar environments, a key step towards ensuring safety is the development of formal methods for modeling, reasoning about, and quantifying uncertainty. Two concrete research directions in this area are:

  1. Correct-by-design construction of systems with learning components.
    The goal of this project is to develop synthesis algorithms for automatically constructing autonomous systems control software that ensures that the risk of unsafe behaviors is within acceptable bounds. The developed synthesis algorithms will account for the uncertainty propagating through the pipeline of components in a system, from the sensors to the control layer. To this end, formal interfaces between these components have to be established, in order to translate system-level safety requirements into constraints on the uncertainty associated with individual components.
  2. Controlling epistemic uncertainty.
    Epistemic uncertainty is uncertainty that stems from the lack of knowledge about the system or the environment in which it operates. This type of uncertainty can be reduced, for example by collecting more data or providing more precise sensors. The goal of this research is to investigate the trade-off between reducing uncertainty on one hand, and cost-effectiveness/performance on the other, and based on that, to develop synthesis algorithms that are guided by the systems safety and task specifications in order to efficiently control the mitigation of epistemic uncertainty.


Thomas Erlebach

Algorithmic Aspects of Comunication Networks. Numerous challenging optimization problems arise in the design and operation of communication networks such as optical networks, cellular wireless networks, mobile wireless ad-hoc networks, and GRID computing. Examples of such problems include network design, resource provisioning, resource allocation, scheduling, virtual backbone construction, and call admission control. Students working on such topics typically identify suitable models and problem formulations, design and analyze algorithms (approximation algorithms, on-line algorithms, distributed algorithms, algorithmic game theory), and implement simulations of algorithms for the purpose of experimental evaluation and comparisons. The focus can be more on the theoretical analysis (proofs of worst-case performance guarantees, competitive analysis) or on the experimental and algorithm engineering side, but typically the research includes aspects of both.

This is a broad topic that can accommodate a number of specific PhD research projects. Note, however, that I already have a number of PhD students and, for the moment, will accept additional students only if they are exceptionally well qualified.

List of skills required:

  • Ability to understand the design and analysis of algorithms.
  • Ability to understand and apply basic concepts of discrete mathematics (graphs, combinatorics, proofs).
  • Ability to write about algorithms and proofs in a precise and rigorous way.
  • Creativity in prolem-solving.
  • Ability to write programs in a suitable programming language such as Java or C++ (only if the PhD project includes a simulation or implementation component).

List of relevant optional modules that can be attended at University of Leicester:

  • CO7200 Algorithms for Bioinformatics
  • CO7212 Game Theory in Computer Science
  • CO7213 Networking and Distributed Computing

Some suggested reading:

  • Introduction to Online Algorithms:
    Susanne Albers: Competitive Online Algorithms. BRICS Lecture Series, LS-96-2, 1996. Available at:
  • Survey of Approximation Algorithms for Disjoint Paths Problems:
    Thomas Erlebach: Approximation Algorithms for Edge-Disjoint Paths and Unsplittable Flow. In E. Bampis et al. (Eds.): Efficient Approximation and Online Algorithms, LNCS 3484, Springer, 2006, pp. 97-134. Available at:
  • Survey of Algorithmic Models of Ad-hoc/Sensor Networks:
    S. Schmid and R. Wattenhofer: Algorithmic Models for Sensor Networks. In Proceedings of the 14th International Workshop on Parallel and Distributed Real-Time Systems (WPDRTS), April 2006. Available at:
  • Example of an algorithmic result for virtual backbone construction in ad-hoc networks:
    Christoph Ambuehl, Thomas Erlebach, Matus Mihalak, Marc Nunkesser: Constant-factor approximation for minimum-weight (connected) dominating sets in unit disk graphs. In Proceedings of the 9th International Workshop on Approximation Algorithms for Combinatorial Optimization Problems (APPROX 2006), LNCS 4110, Springer, 2006, pp. 3-14. Extended version available at:

Thomas Erlebach's homepage and contact details


Stanley Fung

Design and analysis of algorithms, particularly in the areas of

  • Online algorithms
  • Combinatorial optimization
  • Computational biology and bioinformatics

Background in discrete mathematics and algorithms as provided in most CS undergraduate degrees

Suggested MSc modules:
Analysis and Design of Algorithms. provides the above skills. C++ Programming and Advanced Algorithm Design and Game Theory in Computer Science may also be useful.


Stanley Fung's homepage and contact details


Reiko Heckel

Graph Transformation Games

  • for Social Networks
  • for Autonomous Software Agents

The idea is to apply game-theoretic concepts to networks with dynamic topology. E.g., in the case of social networks, the network topology may change by individuals joining or leaving, connecting or breaking up. Networks of autonomous software agents can show similar behaviour.

In both cases it is interesting to understand how local actions of individuals or agents trying to maximise their own goals lead to global outcomes, or vice versa, how incentives for individuals need to be defined in order for desirable global outcomes to become possible.

A network can be seen as a graph, and its evolution over time modelled by graph transformation rules. See for an introduction to graph transformation and google 'social network analysis' to get an idea of the problem.

We have made first steps combining graph transformation with game theory in this contribution focussing on negotiation of features for services slides.

Model Inference

  • for Social Networks
  • for Web, Cloud or Mobile Services

Reverse engineering of models from existing systems helps understanding, analyses and redesign. For example, we have already developed techniques to derive visual contracts (a diagrammatic modelling language based on graph transformation) from existing services or components in Java and we are currently looking into reverse engineering the behaviour Twitter bots.

Similar questions can be asked of a number of platforms, technologies and applications, such as semantic web, cloud technologies, or machine learning applications.

The following references give an idea of our existing work in this area

Feature-oriented Modelling, Analysis and Simulation

Feature models allow to define variants of systems or products.  The same approach is useful in models of social or software systems if we want to reuse more general models by specialising them to specific requirements, e.g., in order to compare versions with or without certain features. This use of feature modelling for model management raises questions for analysis techniques, which are currently not modular enough to support a feature-oriented approach.

We will look at graph transformation models and their analysis though differential equations or simulation, with applications to social sciences, biology, health or software engineering.

Skills Required

Strong background in at least two out of the following three areas is required.

  • OO development (programming and design).
  • theoretical computer science (automata and formal languages, propositional and first order logic, basic set theory).
  • maths (specifically analysis and probability theory).

Reiko Heckel's homepage and contact details


Michael Hoffmann

1. Algorithm with uncertainty: The area of update algorithms for problems with uncertainty is a relative recent developed topic. For most classical algorithms it is assumed that the input is precise. In this model each input might be given in a rough (uncertain) form. The precise value for each input can be obtained for a certain cost. The algorithm has to decide for which input data the the extra costs needs to be paid to solve the underlying problem. Algorithm with uncertainty are rated on cost effective they are.


  • Programming in C++, Java, or similar computer language
  • Knowledge in time and space complexity
  • Knowledge in statistical analysis

Related publication:

  • Thomas Erlebach, Michael Hoffmann, Danny Krizanc, Matu's Mihala'k, Rajeev Raman: Computing Minimum Spanning Trees with Uncertainty. STACS 2008: 277-288T.

2. Online Algorithms: Quota from wikipedia: ( "In computer science, an online algorithm is one that can process its input piece-by-piece, without having the entire input available from the start. In contrast, an offline algorithm is given the whole problem data from the beginning and is required to output an answer which solves the problem at hand. (For example, selection sort requires that the entire list be given before it can sort it.)

As an example of the problem consider the problem of finding a shortest path in a finite connected graph when the graph is unknown and the algorithm receives the node neighbors only when it "enters" the node. It is clear that this problem can not be solved optimally without a simple exhaustive search. Thus, new performance measures have to be introduced, such as competitive analysis, which compares the performance of an online algorithm with that of a hypothetical offline algorithm that knows the entire input in advance."

In this general topic some of my recent research focused on network discovery. Where a structure of the network is not known and by probing certain nodes the whole network will be discovered.


  • Programming in C++, Java, or similar computer language
  • Knowledge in time and space complexity
  • Knowledge in statistical analysis

Related publication:

  • Zuzana Beerliova, Felix Eberhard, Thomas Erlebach, Alexander Hall, Michael Hoffmann, Matu's Mihala'k, L. Shankar Ram: Network Discovery and Verification. IEEE Journal on Selected Areas in Communications 24(12): 2168-2181 (2006)

Michael Hoffmann's homepage and contact details


Genovefa Kefalidou

  • Automation and Virtual Environments (VR): Increased automation levels provide new opportunities for Human-Technology Interactions (HTI) and the design of new interactive interfaces. In physical environments, automation levels tend to be either too conservative or more liberal depending on the application context. The present research will investigate automation levels uptakes within both the physical and virtual environment with an aim to study socio-cognitive behavioural interactions to inform the design of future 'hybrid designs'.
  • Affective Intelligent Maps: In crisis management, operators tend to rely on a number of different types of data and artefacts to deliver sensemaking of crises and prompt decision-making for recovery. A particular type of artefact that is commonly used in crisis situations are maps. The present research will investigate the design and implementation of 'affective intelligent maps' that augment and visualise different types of intelligence to assist crisis management operators in different scenarios. The design is going to be socio-cognitively driven and follow a strong user research approach.
  • Levels of optimisation in Interaction Design (ID): Within Interaction Desigh, we often have 3 major dimensions to consider (though there are more) and these are: text presented on an interface, visuals and physical objects or space. The present research will investigate what are the 'optimal thesholds' of the use of text, visuals and physical space/objects in designing interactive interfaces. A set of case studies will be developed to test different configurations and contexts.
  • Cognitive Sat-Nav: Sat-Navs are, nowadays, well-used within vehicles for navigation purposes and are often highly automated for route calibration. This, however, can result to user disatisfaction, especially, when occurring unexpectedly and while 'on-the-go'. The present research will employ a cognitive-driven and goal-directed design to design and develop a 'Cognitive Sat'Nav' that will allow for more efficient (i.e. user-centred) route optimisation and calibration. Distraction issues and error analyses will be also investigated.
  • The Synaesthesia Machine: Synaesthesia is the term describing the perceptual phenomenon in which stimulation of one sensory or cognitive pathway leads to experiences in another sensory or cognitive pathway. User Experience (UX) relies on sensory input whether this is visual, aural or tactile. The present research will investigate the role of synaesthesia in both physical and virtual environments (VEs) with an aim to understand UX in 'training' contexts where e.g. Virtual Reality (VR) and VEs are heavily used nowadays. Part of this investigation will involve the development of VR intervention(s) that facilitate 'synaesthetic' interactions to measure human performance in training settings.

Genovefa Kefalidou's homepage and contact details


Mohammad Mousavi

  1. Test-case generation for safety analysis of automated vehicle functions
    The introduction of automated and autonomous vehicle functions pose new challenges before traditional safety case analysis and ultimately software and system testing techniques. The complexity of such functions call for a structured method to translate safety goals and driving situations to concrete test cases. The goal of this project is to define and implement a technique that translates structured English safety goals and driving situations into a test-suite and compile the test outcomes into a safety case.
  2. Learning from failures
    Not all failed test cases are deemed significant in practice and many such failures are dismissed on the grounds that they are corner cases and are unlikely to surface in real practice. The goal of this project is to generalise single test case failures into classes of failed test cases and providing a symbolic representation of them.

Mohammad Mousavi's homepage and contact details


Nir Piterman

If you are interested in questions that have to do with two-player games, automata, algorithms related to them, or other things that appear on my research interests, there's something to talk about.

p-Automata and related games: These are new automata motivated by probabilistic CTL and alternating tree automata that accept Markov chains. Their study involve issues about automata (conversion between different transition modes of automata (deterministic, nondeterministic, alternating)), algorithmic questions about automata, the introduction of new games (obligation games) and algorithmic questions about such games.

You can have a look on the paper introducing them or the paper on obligation games .

Synthesis of controllers from temporal specifications: Synthesis (in my language) is the automatic conversion of a specification in linear temporal logic to an input-enabled program all of whose executions satisfy the specification.
This is a question that intrigued researchers in verification for many years, getting much attention, but only recently getting actual practical progress.
The techniques involved in doing this include the study of transition systems, two player games, and construction of strategies. This is also related to automata and temporal logic.
The approach that I have been advocating calls for restricting the type of specifications to a "reasonable" subset that can be handled in practice.

I have recently considered how to apply this to certain abstract ways of representing the world (here).

This is also related to questions about games with partial information, their solutions, and strategies controlling them (See survey, not mine).

Dynamic Reactive Modules: This is an approach for modeling transition systems that support allocation of new processing power (and its deallocation) based on variable sharing (rather than message passing). I find this very exciting as this could be related to ad-hoc networks and such things and hasn't been considered in the past.

See the paper introducing them.

Nir Piterman's homepage and contact details


Rajeev Raman

I am interested in processing, querying and mining very large data. Specific areas include:

  • Efficient Data Structures Niklaus Wirth wrote a famous book in 1976 called Algorithms + Data Structures = Programs. What is meant by this is that algorithms manipulate data, and in order to write a good program, one should identify the operations that one performs on the data and choose an appropriate data structure. However, we are living in a world of BIG data, and classical data structures (such as trees or lists) can be incredibly inefficient.
    • One problem is that normal data structures take up very large amounts of RAM, compared to the data they store. For example, after reading a 1GB XML document into a DOM tree, the memory usage goes up to 15GB RAM. This increase in memory makes it impossible to process BIG data efficiently. Succinct and compressed data structures solve this problem in novel and clever ways. For example, did you know that you can navigate in a binary tree, in which each node is represented using at most two bits?. I have many potential PhD topics in succinct data structures. See an example PhD Thesis I have supervised in this area. There are many practical applications; see e.g. the SiXML project, the Bowtie package.
    • I am also interested in novel algorithms for large-scale data processing, using say MapReduce or similar frameworks, but my interests are narrowly focussed. You will need to provide a general application area (what kind of data are you interested in processing? why is it challenging to process this kind of data using MapReduce?).
  • Data Mining I am interested in data mining. Data mining is of course an application that involves processing large amounts of data. Succinct data structures can help to process large amounts of data. In addition, I am working on two projects:
    • Mining Probabilistic Data. Much of data to be mined is automatically harvested and collected, and is therefore uncertain due to sensor errors, inconsistent data in databases or the web etc. Mining such data is a challenge. See a recent PhD Thesis I supervised on this topic.
    • Tom Gransden, a student supervised jointly with Neil Walkinshaw, is investigating the use of Machine Learning algorithms to detect proof tactics used in Interactive Theorem Provers.


Selected References (my PhD students' names in bold)

  1. Muhammad Muzammal, Rajeev Raman. Mining sequential patterns from probabilistic databases. Knowledge and Information Systems, 2014. 10.1007/s10115-014-0766-7, 2014.
  2. Thomas Gransden, Neil Walkinshaw, Rajeev Raman. Mining State-Based Models from Proof Corpora. CICM 2014: 282-297. Published version on arXiV.
  3. Stelios Joannou, Rajeev Raman. Dynamizing Succinct Tree Representations. Experimental Algorithms Lecture Notes in Computer Science Volume 7276, 2012, pp 224-235. Final submitted version.
  4. Richard Geary, Venkatesh Raman, Rajeev Raman. Succinct ordinal trees with level-ancestor queries. ACM Transactions on Algorithms, 2006, 2 (4), pp.510-534. DOI: 10.1145/1198513.1198516. Final submitted version.

Rajeev's homepage and contact details.


Stephan Reiff-Marganiec

1. Dynamic Adaptation of Workflows: Workflows capture Business Processes, but business is dynamic so their workflows need to adapt. StPowla is an approach to process modelling for service-oriented systems. It has three ingredients: workflows to express core processes, services to perform activities and policies to express variability. Workflows are expressed using a graphical notation. Policies can make short-lived changes to a workflow instance, i.e. they last for the duration of the workflow instance and usually will be made during the execution of the instance, rather than applied to the overall workflow model. There are two types of policies: refinement and reconfiguration. Refinement policies specify criteria for the selection of the service that is ultimately chosen and invoked to execute the task at hand, while reconfiguration policies change the structure of the workflow instance by e.g. deleting or adding tasks. This area also covers the study of policy conflict.

Selected References:

  • S Gorton, C Montangero, S Reiff-Marganiec and L Semini. StPowla: SOA, Policies and Workflows. WESOA 2007.
  • L Bocchi, S Gorton and S Reiff-Marganiec. Engineering Service Oriented Applications: From StPowla Processes to SRML Models. FACS (Formal Aspects of Computing).

2. Service Selection: One area of service-oriented computing is concerned with identifying the right service for a user. This is a very active and interesting area and I am specifically interested in how can the best service for a specific user context be selected and how can the overall selection services for a business process be optimized. In the former area we have developed an extension of LSP (Logic Scoring for Preferences) that allows for automatic ranking of single services. An extension of this method for workflows is under consideration, however, for workflows we are also working on an Immune based algorithm for finding the global best.

Selected References:

  • J. Xu and S Reiff-Marganiec. Towards Heuristic Web Services Composition Using Immune Algorithm. ICWS 2008.
  • HQ Yu and S Reiff-Marganiec. A Method for Automated Web Service Selection. WSCA 2008.

3. Virtual Organisations: The idea of virtual organisations captured the fact that many smaller organisations can work together in dynamic ways to achieve larger goals that none of them could achieve on their own. We are studying how to model VOs at higher levels of abstraction, but in ways that will ultimately allow to reason about their behaviour. A future aspect of this work would be the consideration of a run-time platform to enable the operation of VOs.


  • L. Bocchi, J.L. Fiadeiro, N. Rajper and S. Reiff-Marganiec. Structure and Behaviour of Virtual Organisation Breeding Environments. FAVO 2009.

Stephan Reiff-Marganiec's homepage and contact details


Tom Ridge

I'm interested in ways to make our I.T. systems more dependable and reliable. This could include:

  • developing new programming language features
  • identifying and implementing key I.T. infrastructure, e.g. persistent message queues
  • using mathematics to prove that e.g. implementations of algorithms and systems are correct
  • developing tools to make the above tasks easier e.g. theorem provers such as HOL4, and specification tools such as Ott and Lem

Some concrete current projects I would like PhD students to work on are:

Verified filesystem Filesystems are incredibly important, particularly when applications must provide some form of persistence for their data (eg a database must ensure that data survives a complete system failure). In order to develop applications that use the filesystem, one has to know what guarantees are being provided by the filesystem. Unfortunately current filesystems do not provide many guarantees beyond POSIX "atomic move" (if you move a file, and the system crashes, then either the file moved or it did not). The aim of this project is to develop a filesystem which guarantees certain key properties that application developers depend on. The filesystem will be developed in a functional language such as Haskell, OCaml or SML. Verification will use a theorem prover such as Isabelle, HOL, or Coq. The aim is to develop a reliable filesystem that can be used in real-world systems such as Linux.

Filesystem implementation The project is to develop a C implementation of a filesystem I have implemented in OCaml. The OCaml version is verified correct. Ideally the C implementation would have some direct (formal, mathematical) connection to the OCaml version, so that the C version would also be correct (there are several ways to make this more precise).

Verified computational complexity Lots of effort has been dedicated to reasoning formally about program correctness. We would now like to prove that implemented code has time and space complexity that it is claimed to have. A simple approach would be to define the atomic steps of a language, and count the number of steps a piece of code takes. However, informal reasoning tends to be at a much higher level than this. The aim of this project is to start developing the formal verification of computational complexity by looking at simple functional implementations e.g. of mergesort etc. Some recent work by Bob Harper et al. is relevant, here.

Reasoning above operational semantics One way to prove programs correct is to reason directly about their operational behaviour, as defined by the operational semantics for the language. There are many things that need to be done here, such as developing good operational semantics to support high-level reasoning; developing tools to make symbolic evaluation quicker; developing reasoning techniques for operational reasoning; porting existing techniques to the operational setting etc

Access control matrices Access control matrices (related to access control lists) are used to specify who has access to what resources. For example, the following states that user tom has access to all files, whereas jen has access only to File A.

   |File A|File B|File C
tom|  Y   |  Y   |  Y   
jen|  Y   |  N   |  N

Access control matrices are easy to implement. Unfortunately they are very difficult to manage, because high-level access control rules (e.g. only users with the role of administrator should be able to access all files) are not explicitly captured. Much existing research has been directed at this problem, but it should be possible to do something new and interesting by expressing the high-level rules in higher-order logic, then using automated provers to check that the properties are enforced.


OCaml to C compilation The project is to define how to translate OCaml (more likely, a simple functional programming language such as MiniML) to C. This would provide a general way to achieve the results of the "filesystem implementation" project above. The L4.verified project, to develop a verified operating system, did something similar, and it should be possible to use this existing work.

OCaml to Scheme compilation The project is to define how to translate OCaml (more likely, a simple functional programming language such as MiniML) to Scheme, similar to the OCaml to C compilation project above. Scheme is available pretty much everywhere, but implementations of ML-like languages are not so readily available. When new technologies such as Java (or .NET) come along, you want to be able to use all the new features and technology, combined with everything you love about ML. Scheme is usually supported very quickly e.g. from within Java via JScheme or Kawa, but it is still difficult to use ML-like languages with Java. This project aims to develop an ML to Scheme translator, allowing ML programmers to take advantage of existing Scheme/Java technology to run their ML code on the Java platform.

Tom Ridge's homepage and contact details


Jan Oliver Ringert

Analyses for Understanding Embedded Software Evolution
Embedded software typically executes within a larger system of software and hardware components. Examples of embedded software are found in the avionics, automotive, and robotics domain. These domains are leading adopters of model-based software development where systems are described, analysed, and simulated using software models.

Software models constantly evolve as new requirements are added and bugs are fixed. Efficient means for understanding evolution are paramount for effective change management and maintenance. However, there are still many open questions for the successful application evolution analyses in practice. On the one hand, this project will extend underlying theories to support important concerns of embedded software development, including support for different operation modes and software variants. On the other hand, the project will analyse typical modelling activities and evolution steps of embedded software models. These will be supported with suitable algorithms and means for interaction with engineers to support the analysis and understanding of software model evolution.

Working with Specifications for Reactive Synthesis
Reactive systems are software systems in an ongoing interaction with the environment as found in the robotics and automotive domain. Reactive synthesis presents the appealing idea of the automated construction of software systems from a reactive specification.

With reactive synthesis the task of software engineers shifts from writing code to writing specifications. Currently, there are still many open questions of how to best work with specifications. This project will address some existing challenges. As an example, one focus will be on techniques for testing and analysing (parts of) specifications against expected or previously observed behaviors. As another example, we will investigate meaningful means for the decomposition and reuse of specifications. The outcome will be integrated and evaluated within a toolset for reactive synthesis with focus on autonomous robotic systems.

Jan Oliver Ringert's homepage and contact details



Emilio Tuosto

Abstractions for mobile distributed systems: The widespread use of distributed and concurrent systems urges to use formal models to rigorously describe and analyse computations where remotely executing processes interact through amongcommunication infrastructures that can dynamically change. I'm interested in studying models for several aspects of modern distributed computations from theoretical as well as applied points of view. My favourite models are based on process algebras, automata, and hypergraphs.

1. Process Algebras: Process algebras are particularly suitable for formally describing and reasoning on distributed communicating processes that operates in a dynamically changing environment. Indeed, many different theories (e.g., behavioural type systems) have been shown adequate to tackle modelling and verification problems rising in distributed computing (e.g., distributed coordination, behavioural types, model- or type-checking).

I have been working on calculi featuring event-notification primitives and, more recently, I am interested in applying process algebras to study choreography-based, contracts, and behavioural types of distributed applications.

Required skills: Good mathematical and logical skills. If interested in implementation aspects, good programming skills (either functional or object oriented programming).


  • Robin Milner, Joachim Parrow, David Walker. A Calculus of Mobile Processes Part I and Part II. Information and Computation 100:1-77 (1992).
  • Emilio Tuosto: Contract-Oriented Services. WS-FM 2012: 16-29
  • Laura Bocchi, Hernán C. Melgratti, Emilio Tuosto: Resolving Non-determinism in Choreographies. ESOP 2014: 493-512
  • Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, Roberto Zunino: Honesty by Typing. FMOODS/FORTE 2013: 305-320
  • Julien Lange, Emilio Tuosto: Synthesising Choreographies from Local Session Types. CONCUR 2012: 225-239
  • Roberto Bruni, Ivan Lanese, Hernan Melgratti, Emilio Tuosto. Multiparty sessions in SOC. In D. Lea and G. Zavattaro editors. Coordination Models and Languages, volume 5052 of Lecture Notes in Computer Science, Springer-Verlag, May 2008.
  • GianLuigi Ferrari, Daniele Strollo, Roberto Guanciale, and Emilio Tuosto. Coordination Via Types in an Event-Based Framework. In J. Derrick and J. Vain, editors, 27th IFIP WG 6.1 International Conference on Formal Methods for Networked and Distributed Systems Special focus on service oriented computing and architectures, volume 4574 of Lecture Notes in Computer Science. Springer-Verlag, June 2007.

2. Automata for mobile and distributed applications: Automata are foundamental tools in theoretical computer science as well as in more applied aspects of our discipline. In my research I use automata models to study choregraphy-based design theories as well as nominal automata models. The latter enrich traditional automata to capture computational phenomena arising in mobile applications. Not only automata can be used to check behavioural equivalences of systems, but they are also suitable to design and verify e.g., service compatibility.

Required skills: Good mathematical and logical skills. Notions of automata theory.


  • Robin Milner, Joachim Parrow, David Walker. A Calculus of Mobile Processes - Part I and Part II. Information and Computation 100:1-77 (1992).
  • Alexander Kurz, Tomoyuki Suzuki, Emilio Tuosto: On Nominal Regular Languages with Binders. FoSSaCS 2012: 255-269
  • Alexander Kurz, Tomoyuki Suzuki, Emilio Tuosto: A Characterisation of Languages on Infinite Alphabets with Nominal Regular Expressions. IFIP TCS 2012: 193-208
  • J. Lange, E. Tuosto, N. Yoshida: From Communicating Machines to Graphical Choreographies. POPL 2015
  • G. Ferrari, U. Montanari, E. Tuosto. Coalgebraic Minimisation of HD-Automata for the pi-calculus Using Polymorphic Types. TCS 331:325-365 (2005).
  • V. Ciancia, G. Ferrari, M. Pistore, E. Tuosto. History Dependent Automata for Service Compatibility. In P. Degano, R. De Nicola, and J. Meseguer editors. Concurrency, Graphs and Models, volume 5065 of Lecture Notes in Computer Science, Springer-Verlag, July 2008.

3. Graphs model: Graph and graph transformation can be envisaged as a generalisation of terms and term rewriting. In last years, graphs have been widely used to model concurrent and distributed systems and nowadays many tools rely on such theories. I'm interested in the use of a recent techniques for rewriting hypergraphs, a class of graphs where edges can connect more than 2 nodes. An interesting line of research is the implementation of the rewriting techniques defined for hypergraphs.

Required skills: Good programming skills (preferably functional programming). Some mathematical and logical skills.


  • Kyriakos Poyias, Emilio Tuosto: On Recovering from Run-time Misbehaviour in ADR. ICE 2013: 68-84
  • Kyriakos Poyias, Emilio Tuosto: Enforcing Architectural Styles in Presence of Unexpected Distributed Reconfigurations. ICE 2012: 67-82
  • Gianluigi Ferrari and Dan Hirsch and Ivan Lanese and Ugo Montanari and Emilio Tuosto. Synchronised Hyperedge Replacement as a Model for Service Oriented Computing. F. de Boer, M. M. Bonsangue, S. Graf and W. P. de Roever editors. Formal Methods for Components and Objects: 4th International Symposium, FMCO, volume 4111 of Lecture Notes in Computer Science, Springer-Verlag, November 2005.

Emilio Tuosto's homepage and contact details


Irek Ulidowski

Modelling of reversibility of complex systems: Most simple bio-chemical reactions are in principle reversible, so one might think that such reactions typically fluctuate, going forwards and backwards between a number of states. However, nature is synonymous with change or progress. In nature, reversibility is used in a number of important mechanisms such as, for example, signal passing, recycling of molecular resources and stimulating reactions by catalisys. This project aims at studying the role that reversibility plays in major families of bio-chemical reactions and, more generally, in the behaviour of complex systems, including artificial systems such as distributed or quantum systems, and robotics, with the view to model them formally at an appropriate level of abstraction. It is fairly well known how to model the so-called causal reversibility: we can use process calculi, event structures or modal logics (see publications below). There are, however, more general forms of reversibility, the so-called out-of-causal-order reversibility, that are very crutial in nature as well as in artificial system. But we do not know how to model them appropriately yet. We are currently experimenting with a variety of formal models, including process calculi where processes can change their structure.

  • Iain Phillips, Irek Ulidowski and Shoji Yuen, A reversible process calculus and the modelling of the ERK signalling pathway. Proceedings, Reversible Computation 2012, LNCS, volume 7581, pp. 218-232.
  • Iain Phillips and Irek Ulidowski, Reversibility and asymmetric conflict in event structures. Proceedings of CONCUR 2013, LNCS, volume 8052, pp. 303-318. Springer, 2013. doi:10.1007/978-3-642-40184-8_22
  • Iain Phillips and Irek Ulidowski, An Event Identifier Logic. Mathematical Structures in Computer Science. doi:10.1017/S0960129513000510
  • Irek Ulidowski, Iain Phillips and Shoji Yuen, Concurrency and reversibility. Proceedings, Reversible Computation 2014, LNCS 8507, pp. 1-14. Springer 2014.

Reversible asynchronous cellular automata: The aim of this project is to study what reversibility means for different forms of cellular automata, concentrating on asynchronous cellular automata. Examples of problems that can be studied are the universality questions for families of asynchronous cellular automata, both forwards-only and reversible, where we vary how cells are updated, global versus local reversibility, and the time as well as the direction reversibility of asynchronous cellular automata. An integral part of the project will be a development of a software tool for simulation of reversible asynchronous cellular automata.

  • Daniel Morrison and Irek Ulidowski, Direction-reversible self-timed cellular automata for Delay-Insensitive circuits. Proceedings, ACRI 2014, LNCS, pp. 367-377. Springer 2014.
  • Daniel Morrison and Irek Ulidowski, Arbitration and reversibility of parallel Delay-Insensitive modules. Proceedings, Reversible Computation 2014, LNCS 8507, pp. 67-81. Springer 2014.

Reversible debugging of multi-threaded programs: In the last decade a number of commercial debugging software tools came out that claim to make a full use of reversibility when debugging programs. The most famous example is UndoBD by Undo Software Ltd based in Cambridge, UK. When it comes to dealing with multi-threaded programs or programs that share memory, these state-of-the-art debuggers use a technique called serialisation, which records a run of a multi-threaded program as a "sequence" of instructions. This removes the information about causality, concurrency and mutual exclusion between instructions in different threads. So, in some sense, reversing a run of a multi-threaded program is reduced to backtracking in a serialised run. In general, it is not clear what is the logically and operationally correct form of reversibility here. The situation is complicated further by various optimisation tasks performed during execution, which effectively change the program order. This project aims to explore reversibility of multi-threaded programs by taking the formal methods approach. We aim to develop a robust method for reversing simple multi-threaded programs using a process calculus or event structure-like models. The understanding of reversibility of parallel programs for the purpose of debugging must be reached in the setting of the so-called weak memory models, such as, for example the weak memory model of Java. Also, another issue that reversible debugger developers are concerned with, and which we aim to solve in this project, is multi-threaded recording.

Irek Ulidowski's homepage and contact details


Fer-Jan de Vries

Rewriting and Lambda Calculus We are interested to extend the theory of rewriting with infinite reductions and infinite terms. This leads to new insights when one tries to generalise results and concepts of finite rewriting to the infinite setting. See for papers that I've written with colleagues. Areas that are waiting to be explored are:

  1. Models for infinitary lambda calculus: the study of infinite lambda calculus has revealed an abundance of different syntactic models. Is it possible to construct models that induce the same equality relations as these syntactic models with other means, for instance via domain equations? The converse question is of interest too: given a known semantics of the lambda calculus, what is the corresponding infinite lambda calculus whose term model induces the same equality relation?
  2. Infinite lambda calculi without renaming: traditional finite lambda calculi follow a variable convention. Various solutions have been proposed to circumvent this problem: for instance De Bruijn indices or the Adbmal calculus of Hendriks and van Oostrom. Do these solutions generalise?
  3. Weakly orthogonal rewriting is confluent in finite rewriting. Does this generalise to infinite rewriting?
  4. Undefined terms: for term rewriting and for lambda calculus there is a notion of meaningless set. Meaningless terms need to be identified in order to regain confluence in the infinite orthogonal setting. Is there a notion of meaningless set for other rewriting formats, like Klop's combinatory reduction systems?
  5. Decreasing diagrams is a powerful technique to prove confluence in finite rewriting. Can it be generalised to prove confluence in the infinite setting?#

Fer-Jan de Vries's homepage and contact details


Yu-Dong (Eugene) Zhang

I am interested in deep learning (particularly convolutional neural network) in medical image analysis. Specific areas include:

  • Tumor segmentation is one of the most challenging tasks due to the unpredictable appearance and shape. Our team proposed a deep-learning based approach for segmentation of brain tumors, including tumor core and peritumoral edema. The AI-based delineation for tumors are comparable to or even better than human experts.
  • Detection of Alzheimer’s disease (AD) and mild cognitive impairment (MCI). To differentiate MCI-stable from MCI-converter is important for following treatment. AI technique can help us do this task.
  • Multiple sclerosis (MS) Identification. It is laborious to identify MS in early stage. AI has arrived a good accuracy in our study, and can identify MS patients from healthy controls automatically within seconds.
  • Breast cancer identification in digital mammogram. The abnormal masses in mammogram appear white, so does the dense breast tissues. AI can help capture the neighboring information and help us recognize the abnormal masses from dense breast tissues in an accurate performance.
  • Cerebral microbleeding (CMB) in Susceptibility-weighted imaging (SWI). SWI is more sensitive to detect microbleeding points. Our team proved deep learning can carry out CMB detection and following statistical analysis (area, volume, shape, etc.) within seconds.

Yu-Dong Zhang's homepage and contact details


Huiyu Zhou

Aims of this project are to examine the development of basal-like breast tumours over time in histopathological images and to develop an automated system of analysing histopathological images for basal-like breast cancer detection. We will develop automated deep learning techniques to achieve robust pixel based and patch-based segmentation and classification (e.g. cancer vs. non-cancer regions). Using clinical histopathological images, we will experimentally demonstrate that the proposed basal-like tumour identification system at a system-level can produce more accurate and efficient results than the currently available systems reported in the literature.

Breast cancer is the second most common cause of death in women. The basal-like carcinoma is proposed subtype of breast cancer defined by its gene expression and protein expression profile. Breast cancer is divided into five subtypes, including luminal subtype A, luminal subtype B, normal breast-like subtype, HER-2 overexpression subtype and basal-like subtype. Basal-like tumours are one of five molecularly defined subclasses in breast cancer, and have drawn large attention of researchers because of its limited therapy opportunities. This tumour subtype occurs frequently in younger (<50) patients and constitutes approximately 15% of all breast cancers. Although basal-like tumors are characterized by distinctive morphologic, genetic, immunophenotypic, and clinical features, neither an accepted consensus on routine clinical identification and definition of this aggressive subtype of breast cancer nor a way of systematically classifying this complex group of tumors has been described. Therefore, we here propose a new deep learning based approach for improving the accuracy of basal-like breast cancer detection.

List of skills required:

  • Ability to understand the design and analysis of algorithms.
  • Ability to understand and apply basic concepts of machine learning and AI.
  • Ability to present and write in English.
  • • Ability to write programs in Java, C++/C, Matlab or Python.

Suggested readings:

  • Zhang, K., Crookes, D., Diamond, J., Fei, M., Wu, J., Zhang, P. and Zhou, H. "Multi-scale colorectal tumour segmentation using a novel coarse to fine strategy". Proc. Of BMVC, 2016.
  • Moyes, A., Zhang, K., Crookes, D., Ji, M., Wang, L. and Zhou, H. "A novel method for unsupervised scanner-invariance using a dual-channel auto-encoder model". Proc. Of BMVC, 2018.

Huiyu Zhou's homepage and contact details


Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc
E: MSc

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom


DisabledGo logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.