PhD in Formal Verification of Distributed Systems (1.0 FTE) (V25.0493)

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.

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).

o Model checking and automata theory.o SAT, SMT, and CHC solving.
o Temporal logic and TLA+.
o Distributed algorithms, blockchains, and smart contracts.
o 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.

Application should include:

• Letter of motivation (describing interest and qualifications for the research direction(s) of choice).
• CV (including contact information for at least two academic references).
• Transcripts from your Bachelor’s and Master’s degree.

You can submit your application until 20 October 11:59pm / before 21 October 2025 Dutch local time (CET) by means of the application form (click on "Apply" below on the advertisement on the university website).

Applications received before 21 October 2025 will be given full consideration; however, the position will remain open until it is filled.

The University of Groningen strives to be a university in which students and staff are respected and feel at home, regardless of differences in background, experiences, perspectives, and identities. We believe that working on our core values of inclusion and equality are a joint responsibility and we are constructively working on creating a socially safe environment. Diversity among students and staff members enriches academic debate and contributes to the quality of our teaching and research. We therefore invite applicants from underrepresented groups in particular to apply. For more information, see also our diversity policy webpage: https://www.rug.nl/about-ug/policy-and-strategy/diversity-and-inclusion/

Our selection procedure follows the guidelines of the Recruitment code (NVP): https://www.nvp-hrnetwerk.nl/nl/sollicitatiecode and European Commission's European Code of Conduct for recruitment of researchers: https://euraxess.ec.europa.eu/jobs/charter/code

Unsolicited marketing is not appreciated.