PhD in Formal Verification of Distributed Systems
Formal verification aims at providing strong guarantees about the behaviour of programs and systems. It relies on logic to precisely describe the system in question and check desired properties, with both academia and industry recognising its importance.
Distribution is an integral part of innumerous computer systems, providing them with essential improvements to aspects such as performance and fault-tolerance. Due to the critical nature of many distributed systems, their correctness is of crucial importance. The verification of distributed systems, however, is notoriously difficult.
This PhD research is envisioned to broadly follow one of three directions, but can be adapted to suit the interests of an excellent applicant.
- The use of formal languages to specify and reason about distributed systems has been an object of intensive research. While verification support for these languages does exist, it is limited in either the guarantees it can provide or in its level of automation. Lifting this limitation is a clear goal, with a potential target language being TLA+.
- The advent of smart contracts, programs deployed on blockchain platforms, promises to significantly change how financial assets are manipulated. They are likely targets of attacks, with unintended behaviours being exploited to affect assets estimated in millions of US Dollars. Ensuring that contracts cannot be exploited is critical. The goal is to develop a language-agnostic verification approach, following on promising results related to the Solidity language.
- While our current digital infrastructure relies on classical networks, quantum networks are slowly becoming a reality. The coordination algorithms that govern their operation are unlike those employed in classical networks, necessitating novel verification approaches. The goal is to design an automated reasoning approach in tandem with ongoing formalisation efforts, with a focus on probabilistic behaviours.
The objective of the temporary position is the production of a number of research articles in peer-reviewed scientific journals and conference proceedings, which together will form the basis of a thesis leading to a PhD degree (Dr) at the University of Groningen.
Organisation
Founded in 1614, the University of Groningen enjoys an international reputation as a dynamic and innovative institution of higher education offering high-quality teaching and research. Flexible study programmes and academic career opportunities in a wide variety of disciplines encourage the 33,000 students and researchers alike to develop their own individual talents. As one of the best research universities in Europe, the University of Groningen has joined forces with other top universities and networks worldwide to become a truly global centre of knowledge.
Within the Faculty of Science and Engineering, a 4-years PhD position is available at the Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence with the topic of formal verification of distributed systems. The candidate would become a member of the Fundamental Computing Group of the Computer Science Department and would work under the supervision of Dr Rodrigo Otoni.
