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.