PhD "Verified Probabilistic Verification" (VPV)
We are looking for an excellent candidate for a PhD project (for 4 years) on verifying the correctness of probabilistic model checking algorithms and tools as …
- Drienerlolaan, Enschede, Overijssel
- Tijdelijk contract / Tijdelijke opdracht
- Uren per week:
- 38 - 38 uur
- € 2395 - € 3061 per maand
We are looking for an excellent candidate for a PhD project (for 4 years) on verifying the correctness of probabilistic model checking algorithms and tools as part of the "Verified Probabilistic Verification" (VPV) project funded by NWO, the Dutch Research Council.
Probabilistic model checking (PMC) is a technique for the automated analysis of probabilistic models representing complex safety- or performance-critical systems with random uncertainties. So far, the algorithms used in PMC have been proven correct on paper and tool implementations have been tested on a limited number of standard examples. The goal of the VPV project is to use interactive theorem provers like Isabelle/HOL to create machine-checked correctness proofs for core PMC algorithms such as sound value iteration on Markov decision processes. From these proofs, we want to derive correct-by-construction probabilistic verification tools. Additionally, we plan to formalise the semantics of probabilistic modelling formalisms like Modest or JANI, develop new verification algorithms that use exact rational arithmetic to avoid floating-point errors and implement techniques to derive large benchmark examples from small challenges verified by the correct-by-construction tool.
While the work of the VPV project takes place at the University of Twente, there is ample opportunity for visits to partner institutes with specific expertise related to the project goals, for example in the Netherlands, Germany, and Argentina.
We are looking for an enthusiastic student with an M.Sc. degree (or equivalent) in Computer Science, or in Mathematics with a demonstrable interest in computer science, or who is about to obtain such a degree before the start date of the project. The candidate should have a thorough theoretical background, an interest in probabilistic models and theorem proving and ideally some prior experience with formal methods, probability theory, and/or interactive theorem provers. The working language at the University of Twente is English and we expect demonstrated excellence in communicating in English on an academic level.
- A PhD position for 4 years (38 h/week).
- An outstanding scientific environment: our research group was ranked 1st in the last national research assessment.
- Full status as an employee at the University of Twente, including pension and health care benefits.
- Gross salary PhD student: ranging from € 2.395,00 (1st year) to € 3.061,00 (4th year) per month, plus holiday allowance (8%) and end-of-year bonus (8.3%).
- Extensive opportunities for professional and personal development.
- Good secondary conditions, in accordance with the collective labour agreement CAO-NU for Dutch universities.
- A green and lively campus, with excellent sports facilities and many other activities.
Starting date of the position: as soon as possible, January 2021 at the latest.