Applications will be evaluated on a monthly basis. The vacancy may be closed early once the 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’s goal is to create new highly-reliable approaches – languages, algorithms, and tools – for the modelling and analysis of complex systems subject to uncertainty. The project’s mathematical foundations are extensions of continuous-time Markov chains and Markov decision processes. Its approach is the development of sound, fast, and provably correct algorithms with the assistance of interactive theorem provers.

As Ph.D. student on TruSTy, you will develop new approaches for sound probabilistic model checking (typically based on numeric fixpoint algorithms and implemented via floating-point arithmetic with carefully managed rounding) or statistical model checking (exploiting and extending the decades of research in statistics for application in our domain). You will carefully balance algorithm performance and scalability with numeric accuracy requirements. To prove the correctness of your algorithms, you can use the Isabelle interactive theorem prover; with the Isabelle Refinement Framework, you can turn your proofs into high-performance and correct-by-construction executable LLVM bytecode. The results of your research 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 guided and supervised by senior researchers that are experts in probabilistic and statistical model checking (Arnd Hartmanns) and interactive theorem proving (Peter Lammich). You will have the opportunity to work together

• with your fellow TruSTy Ph.D. candidate
• with local Ph.D. students and postdocs on related projects (who, for example, will apply your work to improve the reliability of critical water infrastructures such as storm surge barriers)
• with Ph.D. students and researchers in the Dutch IPA research school, and
• in an international community of formal methods researchers with the possibility for stays abroad at our partner institutes in Germany, Argentina, China, and other countries.

• You are an enthusiastic and highly motivated student with the goal of excelling 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 – by way of advanced courses or individual academic projects – in at least two of the following subject areas:
• 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 a good team spirit and like to work in a diverse and internationally-oriented environment
• You are proficient in English.

• As a PhD candidate at the University of Twente, 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.
• You will be a member of the Formal Methods and Tools group, a strong research group on formal verification with an open and welcoming atmosphere.
• 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.872,- (first year) to € 3.670,- (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 annual leave hours (29 days) in case of full-time employment based on a formal work week of 38 hours. A full-time employment in practice means 40 hours a week, therefore resulting in 96 extra leave hours (12 days) on an annual basis.
• Free access to sports facilities on a green 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.

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

The group consists of approximately 40 researchers with a very diverse background. We have an open and inclusive atmosphere, with many group activities (both work-related and fun).

Are you interested in this position? Please send your application via the 'Apply now' button below, and include:

• A brief cover letter (1 page A4) that explains your motivation to apply for a Ph.D. trajectory in general as well as for 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 (on the 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 of your own.
• The names, affiliations, and email addresses of 2 academic references who can be contacted for additional information about you. Do not include recommendation letters: We will contact your references ourselves if needed.

Applications will be evaluated on a monthly basis. The vacancy may be closed early once the positions are filled.