项目介绍

2025年5月3日

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.

Your profile

• You have, or will shortly acquire, a MSc, degree in Computer Science, Mathematics, or a related field.
• You have a creative mindset and strong problem-solving and analytical skills.
• You have a strong affinity with formal methods, logic, program verification, or related fields.
• You are interested in learning more and working with topics such as: coalgebras, session types, causal reasoning, liveness analysis, and recovery techniques for interacting systems.
• You are fluent in English and have excellent communication skills.
• You have good team spirit and like to work in an interdisciplinary and internationally oriented environment.

Our offer

• As a PhD candidate at UT, you will be appointed to a full-time position for four years, with a qualifier in the first year, within a very stimulating and exciting scientific environment;
• The University offers a dynamic ecosystem with enthusiastic colleagues;
• Your salary and associated conditions are in accordance with the collective labour agreement for Dutch universities (CAO-NU);
• You will receive a gross monthly salary ranging from € 2.901,- (first year) to € 3.707,- (fourth year);
• There are excellent benefits including a holiday allowance of 8% of the gross annual salary, an end-of-year bonus of 8.3%, and a solid pension scheme;
• The flexibility to work (partially) from home;
• A minimum of 232 hours in case of full-time employment based on a formal workweek of 38 hours. A full-time employment in practice means 40 hours a week, therefore resulting in 96 extra leave hours on an annual basis.
• Free access to sports facilities on campus
• A family-friendly institution that offers parental leave (both paid and unpaid);
• You will have a training programme as part of the Twente Graduate School where you and your supervisors will determine a plan for a suitable education and supervision;
• We encourage a high degree of responsibility and independence while collaborating with close colleagues, researchers and other staff.

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