Job Description

Applications will be evaluated monthly. The vacancy may close early once positions are filled.

We offer two Ph.D. positions within the TruSTy project on “Trustworthy Analysis of Stochastic Timed Systems” funded by NWO, the Dutch Research Council. The project aims to develop highly reliable approaches – languages, algorithms, and tools – for modeling and analyzing complex systems under uncertainty. The project's mathematical foundations extend continuous-time Markov chains and Markov decision processes, focusing on creating sound, fast, and provably correct algorithms using interactive theorem provers.

As a Ph.D. student in TruSTy, you will develop new methods for sound probabilistic model checking (based on numeric fixpoint algorithms and implemented via floating-point arithmetic with careful rounding management) or statistical model checking (leveraging decades of research in statistics for our domain). You will balance algorithm performance and scalability with numeric accuracy requirements. Using the Isabelle interactive theorem prover, you can prove the correctness of your algorithms and convert these proofs into high-performance, correct-by-construction executable LLVM bytecode. Your research outcomes will be integrated into the Modest Toolset, a comprehensive suite of quantitative verification tools developed and maintained by the TruSTy team since 2008.

Your work will be supervised by senior researchers who are experts in probabilistic and statistical model checking (Arnd Hartmanns) and interactive theorem proving (Peter Lammich). You will collaborate with:

• Your fellow TruSTy Ph.D. candidate
• Local Ph.D. students and postdocs on related projects, such as improving the reliability of critical water infrastructures like storm surge barriers
• Ph.D. students and researchers in the Dutch IPA research school
• An international community of formal methods researchers, with opportunities for stays abroad at partner institutes in Germany, Argentina, China, and other countries

Your Profile

• You are an enthusiastic and highly motivated student aiming to excel in research.
• You have or will soon acquire a Master's degree (or equivalent) in Computer Science, Mathematics, or a related field.
• You have demonstrable experience in at least two of the following areas through advanced courses or individual academic projects:

- Formal methods, verification, and model checking
- Interactive theorem proving
- Algorithms and data structures
- Probability theory and statistics

• You have strong programming skills in an object-oriented or systems language (C, C++, C#, Rust, or Java)
• You are enthusiastic about working at the intersection of Computer Science and Mathematics
• You have good teamwork skills and enjoy working in a diverse, internationally-oriented environment
• You are proficient in English

Our Offer

• A full-time Ph.D. position for four years, with a qualifier in the first year, within a stimulating and exciting scientific environment at the University of Twente
• Membership in the Formal Methods and Tools group, a leading research group in formal verification with an open and welcoming atmosphere
• A dynamic ecosystem with enthusiastic colleagues
• A salary in accordance with the collective labor agreement for Dutch universities (CAO-NU), ranging from €2,872 gross per month (first year) to €3,670 gross per month (fourth year)
• Excellent benefits, including an 8% holiday allowance, an 8.3% end-of-year bonus, and a solid pension scheme
• Flexibility to work partially from home
• A minimum of 232 annual leave hours (29 days) for full-time employment based on a 38-hour workweek, with an additional 96 extra leave hours (12 days) annually due to a 40-hour workweek in practice
• Free access to sports facilities on a green campus
• A family-friendly institution offering both paid and unpaid parental leave
• A training program as part of the Twente Graduate School, where you and your supervisors will create a tailored education and supervision plan
• Encouragement of high responsibility and independence, while collaborating with colleagues, researchers, and other staff

Information and Application

Interested in this position? Please apply via the 'Apply now' button below and include:

• A brief cover letter (1 page A4) explaining your motivation for applying for a Ph.D. and this specific position, and your prior experience with verification, model checking, or interactive theorem proving
• A Curriculum Vitae
• A transcript of all courses attended and grades obtained (Bachelor’s and Master’s level or equivalent), and, if applicable, a list of publications
• A PDF version of your Master’s thesis or comparable work
• The names, affiliations, and email addresses of two academic references who can provide additional information about you. Do not include recommendation letters: We will contact your references if needed.

Applications will be evaluated monthly. The vacancy may close early once positions are filled.

About the Department

The Formal Methods and Tools group is part of the Computer Science department at the University of Twente. Our mission is to develop mathematical methods, high-performance data structures and algorithms, and suitable programming languages for designing reliable software- and data-intensive control systems.

The group consists of approximately 40 researchers with diverse backgrounds. We maintain an open and inclusive atmosphere with many group activities, both work-related and social.

About the Organization

The Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) at the University of Twente uses mathematics, electronics, and computer technology to advance Information and Communication Technology (ICT). As ICT is integral to nearly every device and product today, we embrace our role in contributing to a wide range of societal activities and pioneering the digital society of tomorrow. Our faculty collaborates extensively with industrial partners and researchers in the Netherlands and abroad, conducting high-profile research for external commissioning parties and funders. Our research is accommodated in three multidisciplinary UT research institutes: Mesa+ Institute, TechMed Centre, and Digital Society Institute.