Are you interested in developing ground-breaking techniques to verify the correctness of software, and do you think parallel computing is exciting? In the GAP project, you can do research on how to use graphics processors to drastically improve the performance of probabilistic model checking, a technique to systematically analyse systems with probabilistic behaviour.

The Software Engineering & Technology cluster at Eindhoven University of Technology (TU/e) offers one PhD position on the development of GPU accelerated probabilistic model checking techniques, within the NWO Open Competition project
GAP: GPU Accelerated Probabilistic Model Checking of Information and Communication Systems.

DESCRIPTION

Probabilistic model checking (PMC) is a technique to systematically analyse systems with probabilistic behaviour. PMC is successfully applied for various purposes, such as to verify the correctness of hard- and software systems in which random phenomena play a role, to perform reliability engineering using fault tree analysis, and to synthesise controller software. However, since the state spaces constructed during PMC tend to grow rapidly, PMC can be very time consuming. In the GAP project, we will conduct research on using graphics processors (GPUs) to perform PMC. Due to the particular architecture of GPUs, this is very challenging and non-trivial.

The GAP project is led by dr.ing. Anton Wijs. At the TU/e, he develops model checking techniques that are accelerated by the use of graphics processing units (GPUs). GPUs offer great potential for parallel computation, while keeping power consumption low. However, not all types of computation can trivially be performed on GPUs, sometimes the algorithms need to be entirely redesigned. In earlier work, we were the first to demonstrate that GPUs can accelerate state space
generation hundreds of times, and therefore that there is potential for a major model checking computational boost. In addition, we have shown that by only accelerating the probability computations, the entire PMC procedure can already become significantly faster. We will use these insights for the next major step: the effective execution of complete PMC on GPUs.

We will extend our state space exploration engine to support probability distributions, and thereby enable PMC. We will focus on the explicit approach to verify Discrete Time Markov Chains (DTMCs) w.r.t. probabilistic CTL properties, as other variants of PMC provide the same computational challenges. Especially the step from detecting all reachable states to the creation of a DTMC will be challenging to perform efficiently using thousands of GPU threads. 
Furthermore, we will investigate the symbolic verification of DTMCs. For this, we will focus on Multi-Terminal Binary Decision Diagrams (MTBDDs). This is the most challenging part of the project. Manipulating BDDs on a GPU has received some attention in related work, but we will be the first to focus on MTBBDs, and the first to integrate the manipulation of them into GPU PMC computations.

The research will be conducted in the Software Engineering & Technology (SET) cluster of the Computer Science department at TU/e. The SET cluster develops methods and tools for time- and cost-efficient evolution of high-quality software systems. In the same department, The Formal System Analysis group has experts on techniques to model and analyse discrete system behaviour in a mathematically rigorous way. Finally, the PhD student is expected to work with and visit the Software Modeling and Verification group at RWTH Aachen University in Germany. In this group, the probabilistic model checker Storm is developed and maintained.

We are looking for candidates that meet the following requirements:

• MSc in Computer Science or Electrical Engineering.
• Experience in, and enthusiasm for, programming (not necessarily parallel programming).
• Good communicative skills in English, both in speaking and writing. Candidates should be prepared to prove their English language skills.

Besides the above requirements, the candidate should also fit at least one of the two following
profiles:

1. The candidate has knowledge of formal verification and experience in the involved algorithms, and is interested in programming GPU applications to speed up model checking. This includes having an interest in learning about the hardware characteristics of GPUs, and how to optimise applications that run on them.
2. The candidate has knowledge of parallel programming / high performance computing (not necessarily GPU programming in particular), and is interested in learning about formal verification. This includes in particular learning the theory of (probabilistic) model checking. At TU/e, courses are offered on this topic that can be attended by the candidate.

Candidates that fit both profiles are particularly encouraged to apply.

We offer

A meaningful job in a dynamic and ambitious university, in an interdisciplinary setting and within an international network. You will work on a beautiful, green campus within walking distance of the central train station. In addition, we offer you:

• A research position in an internationally renowned research group.
• Full-time employment for four years, with an intermediate evaluation (go/no-go) after nine months. You will spend 10% of your employment on teaching tasks.
• Salary and benefits (such as a pension scheme, paid pregnancy and maternity leave, partially paid parental leave) in accordance with the Collective Labour Agreement for Dutch Universities, scale 27.
• A year-end bonus of 8.3% and annual vacation pay of 8%.
• High-quality training programs and other support to grow into a self-aware, autonomous scientific researcher. At TU/e we challenge you to take charge of your own learning process.
• An excellent technical infrastructure, on-campus children's day care and sports facilities.
• An allowance for commuting, working from home and internet costs.
• A Staff Immigration Team and a tax compensation scheme (the 30% facility) for international candidates.

Because even when you are far from home, we feel it is important for you to feel at home.