The School of Computer Science at the University of Birmingham, UK, is continuously looking for strong PhD candidates. One particular field of interest is the design of distributed systems, such as blockchain systems, and their formal verification. This is an important research area for the simple reason that our society strongly depends on distributed critical information infrastructures such as distributed public ledgers, electrical grids, autonomous vehicles, etc. These systems are required to operate in increasingly more complex environments (with malicious participants, time constraints, etc.). This makes designing and ensuring that they operate correctly a challenging task.
This is a large field of study, which encompasses several areas such as distributed systems, formal methods, and programming languages, among others. It raises many interesting questions and challenges. Topics of particular interest are, for example:
• Design and formal verification of Byzantine fault-tolerant (e.g., blockchain) systems
• Design and probabilistic formal verification of distributed real-time systems
• Type theory applied to the design and verification of distributed systems
• Logical foundations of distributed systems
• Knowledge reasoning applied to the verification of distributed systems
In particular, one challenge that we are currently facing is that the spectrum of fault and system models used to design, specify and reason about distributed systems is very wide (from benign to arbitrary faults; from synchronous to fully asynchronous systems) to encompass the wide range of environments in which distributed systems are meant to run in, making developing general verification techniques challenging.
Therefore, possible project are: (1) to develop fault-tolerant distributed systems that can execute correctly in emerging environments (in particular malicious or real-time environments); and (2) to develop models and proof techniques to help reason about a wide variety of distributed systems. It is a prerequisite to prove the formal correctness of distributed systems, and is challenging for sophisticated and realistic models, such as probabilistic models, or hybrid models that mix different types of faults and systems.
Regarding (1), we propose to investigate novel efficient designs of fault-tolerant systems that can sustain persistent attacks, and/or can provide real-time guarantees. Regarding (2), we propose to investigate how to formally capture realistic fault and system models in a way that facilitates the study of systems in various environments, and to develop proof techniques to help verify the correctness of distributed systems in those models.
Eligibility: First or Upper Second Class Honours undergraduate degree and/or postgraduate degree with Distinction (or an international equivalent). We also consider applicants from diverse backgrounds that has provided them with equally rich relevant experience and knowledge. Full-time and part-time study modes are available.
Excellent problem solving skills and programming skills are required. In addition, the candidate must have a strong background in one of the following areas:
* Formal methods
* Distributed systems
* Programming languages
* Type theory
If your first language is not English and you have not studied in an English-speaking country, you will have to provide an English language qualification.
Continue with Facebook
