Programs often suffer from liveness issues - they may get stuck or fail to make progress. How can we address this? Our approach is to apply foundational techniques grounded in logic, semantics, and verification. This work takes place within the CYCLIC project: Cyclic Structures in Programs and Proofs, a collaboration among five Dutch universities: the University of Twente, the University of Groningen, Leiden University, Radboud University, and Delft University.
The Formal Methods and Tools (FMT) group at the University of Twente is looking for a highly motivated and talented PhD candidate to join our team. In this position, you will explore advanced frameworks to make complex interacting programs fault-tolerant and future-proof. You will contribute to the CYCLIC project: Cyclic Structures in Programs and Proofs, a collaboration among five Dutch universities, uniting experts in cyclic structures, coinduction, program verification, and proof assistants.
Your focus will be on developing frameworks that pinpoint and explain the root causes of failures in interacting programs - a key step towards ensuring fault-tolerance. While existing methods address safety (e.g., via reachability), reasoning about liveness remains challenging.
You will design causal frameworks to detect, explain, and support recovery from liveness violations. These frameworks will:
- Identify the causes and responsible agents of liveness breaches, and assess any resulting harm.
- Support recovery strategies using counterfactual reasoning (“what if?”), guiding programs back to valid operational states.
Your starting point will be identifying realistic constraints (such as fairness assumptions and timeout mechanisms) that allow for effective liveness analysis via extensions of coalgebraic session types, which model the behaviour of communication channels. Building on this, you will develop a formal notion of causality by connecting behavioural maps of extended coalgebraic sessions with established causal models. Ultimately, you will design algorithms for causality-based analysis and counterfactual recovery of liveness violations.
Information and application
Are you interested in this position? Please send your application via the 'Apply now' button below before May 24, 2025. The link will redirect you to the centralised recruitment page of the consortium. Choose “PhD position 4: Liveness from causality analysis (Twente)” to apply for this specific vacancy.
For more information regarding this position, you are welcome to contact Georgiana Caltais (g.g.c.caltais@utwente.nl).
About the organisation
The faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) uses mathematics, electronics and computer technology to contribute to the development of Information and Communication Technology (ICT). With ICT present in almost every device and product we use nowadays, we embrace our role as contributors to a broad range of societal activities and as pioneers of tomorrow's digital society. As part of a people-first tech university that aims to shape society, individuals and connections, our faculty works together intensively with industrial partners and researchers in the Netherlands and abroad, and conducts extensive research for external commissioning parties and funders. Our research has a high profile both in the Netherlands and internationally. It has been accommodated in three multidisciplinary UT research institutes: Mesa+ Institute, TechMed Centre and Digital Society Institute.
Want to know more?
