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.
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:
Besides the above requirements, the candidate should also fit at least one of the two following
Candidates that fit both profiles are particularly encouraged to apply.
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:
Because even when you are far from home, we feel it is important for you to feel at home.
Eindhoven University of Technology is an internationally top-ranking university in the Netherlands that combines scientific curiosity with a hands-on attitude. Our spirit of collaboration translates into an open culture and a top-five position in collaborating with advanced industries. Fundamental knowledge enables us to design solutions for the highly complex problems of today and tomorrow.
Curious to hear more about what it’s like as a PhD candidate at TU/e? Please view the video.
For more information about the project, please contact dr.ing. Anton Wijs, e-mail: A.J.Wijs[at]tue.nl.
Are you inspired and would like to know more about working at TU/e? Please visit our career page.
We invite you to submit a complete application by using the 'apply now'-button on this page.
The application should include:
Please apply by using the ‘Apply now’ button on this page. You can upload a maximum of 5 documents (max. 2 MB each).