"PhD in Formal Verification of Distributed Systems (1.0 FTE)"

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.

The successful candidate should:

• Have (or be close to completing) an MSc in computer science or a related field.
• Have an interest in both theory and practice.
• Have strong programming skills and interest in developing state-of-the-art tools.
• Have excellent communication skills in English (both oral and written).
• Preferably have experience in (some of) the topics below (not a strict requirement).
  • Model checking and automata theory.
  • SAT, SMT, and CHC solving.
  • Temporal logic and TLA+.
  • Distributed algorithms, blockchains, and smart contracts.
  • Quantum information theory and Markov decision processes.

We offer you, following the Collective Labour Agreement for Dutch Universities:

• A salary of € 3,059 gross per month in the first year, up to a maximum of € 3,881 gross per month in the fourth and final year for a full-time working week
• A holiday allowance of 8% gross annual income and an 8.3% year-end bonus
• Teaching: employed PhD candidates are expected to spend 10% of their working hours on teaching and/or supervising candidates
• A full-time position (1.0 FTE). The successful candidate will first be offered a temporary position of one year with the option of renewal for another three years. Prolongation of the contract is contingent on sufficient progress in the first year to indicate that a successful completion of the PhD thesis within the next three years is to be expected. A PhD training programme is part of the agreement and the successful candidate will be enrolled in the Graduate School of Science and Engineering.