About the Project
The School of Computer Science at the University of Birmingham, UK, is looking for strong PhD candidates. One particular field of interest is formal methods applied to distributed systems. This is a critical area of study for the evident reason that our society strongly depends on distributed critical information infrastructures such as electrical grids, autonomous vehicles, distributed public ledgers, etc. Unfortunately, the systems being developed nowadays are increasingly more complex, which makes ensuring that they operate correctly a very challenging task.
This is a very large field of study, which encompasses different 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:
* Formal verification of Byzantine fault-tolerant systems
* Probabilistic formal verification of distributed real-time systems
* Using knowledge reasoning to verify distributed systems
* Using type theory to verify distributed systems
* Logical foundations of distributed systems
In particular, one challenge that we are currently facing is that the spectrum of fault models and system models used to specify and reason about distributed systems is very wide (from benign to arbitrary faults; from synchronous to fully asynchronous systems), as various kinds of distributed systems are meant to work in various kinds of environments (such as cloud-based systems, IoT systems, safety critical real-time systems, ...). Another challenge is that widely different proof techniques are typically used to reason about different fault/system models.
Therefore, one possible project could be to develop models and proof techniques to help reason about a wide variety of distributed systems. Formally defining these models is a non-trivial task. It is however a prerequisite to prove the formal correctness of distributed systems. Some work has already been done to tackle standard models (such as fully synchronous or fully asynchronous), but much remains to be done to handle more sophisticated and realistic models, such as, for example, probabilistic models, or hybrid models that mix different fault/system.
We propose here to investigate how to formally capture such intricate, though more realistic, fault/system models, in a way that facilitates the study of systems in various environments. In addition, we propose to develop proof techniques to help verify the correctness of distributed systems in those models. It is rapidly becoming vital to develop such formal tools, given the advance of critical technologies, such as the blockchain technology, or the autonomous vehicle infrastructure.
Funding Notes
The position offered is for 3.5 years full-time study. The value of the award is stipend: £15,009 pa; tuition fee: £4,327.
Eligibility: 2:1 Honours undergraduate degree and/or postgraduate degree with Distinction (or an international equivalent) in Computer Science. 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.
References
Rahli, V., Vukotic, I., Völp, M. and Esteves-Verissimo, P., 2018, April. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In European Symposium on Programming (pp. 619-650). Cham: Springer. http://www.cs.bham.ac.uk/~rahliv/articles/velisarios.pdf
http://www.cs.bham.ac.uk/~rahliv