PhD on GPU accelerated symbolic reasoning about software systems

Are you fascinated by the large role software plays in today’s society? Are you eager to contribute to improving software development, and making it more structured, resulting in high-quality, functionally correct software?

We offer one fully funded PhD position on GPU accelerated techniques to reason about, and automatically construct, software.

Information
Supervisory controllers that integrate the behaviour of subsystems into meaningful and expected behaviour play an increasing role in the operation of high-tech systems and cyber-physical systems. Supervisory Controller Synthesis is an engineering approach to automatically derive a supervisory controller for a given system model that is safe w.r.t. certain requirements. Currently, it works for systems that can be described by discrete event models. However, there are severe computational limitations when applying synthesis to industrial size case studies. This is related to the enormous size of the state space of such systems, i.e., the number of different states the systems can be in.

GPU-acceleration has great potential to be an important step forward in this field. In the GUESS project, symbolically reasoning about these state spaces using GPUs will be addressed. In doing so, we expect to go far beyond existing work, not only on Supervisory Controller Synthesis, but also other applications relying on similar computations, such as model checking, automated planning, and reliability engineering.

The project will primarily contribute to reliable and safe-by-construction supervisory controllers for infrastructural objects such as waterway locks, sluices, tunnels, bridges and roadside systems. On top of increased safety, the developed techniques also contribute to the easier and more affordable development and maintenance of such systems. In addition, the project is expected to contribute to automatically checking software correctness, which is a primary concern for many software development companies.

Working on this topic as a PhD student, you will be a member of the Parallel Software Development group (PSD, see http://psd.win.tue.nl), which is part of the Software Engineering & Technology cluster (SET) of the Mathematics and Computer Science department. The members of this group conduct research on accelerated automated reasoning, often using GPUs. As such, you will be able to discuss your research and brainstorm with your fellow group members. In addition, a second GUESS PhD student will work in the Supervisory Control group (see https://www.tue.nl/en/research/research-groups/control-systems-technology/group-supervisory-control) , which is part of the Control Systems Technology section of the Mechanical Engineering department. This PhD student will focus on developing Supervisory Controller Synthesis algorithms, and together, you will be able to develop your results into groundbreaking tools for Supervisory Controller Synthesis.

• A master’s degree (or an equivalent university degree) in Computer Science.
• Experience in, and enthusiasm for, programming (not necessarily parallel programming).
• A research-oriented attitude.
• Ability to work in an interdisciplinary team.
• Motivated to develop your teaching skills and coach students.
• Fluent in spoken and written English (C1 level).

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 (symbolic) state space exploration. 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 and related theory and algorithms. This includes, in particular, learning the theory of Supervisory Controller Synthesis. At TU/e, relevant courses are offered that can be attended by the candidate.

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:

• Full-time employment for four years, with an intermediate assessment after nine months. You will spend a minimum of 10% of your four-year employment on teaching tasks, with a maximum of 15% per year of your employment.
• 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 P (min. € 2,901 max. € 3,707).
• 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.

Do you recognize yourself in this profile and would you like to know more? Please contact the hiring manager Anton Wijs, Associate Professor (A.J.Wijs@tue.nl).

Visit our website for more information about the application process or the conditions of employment. You can also contact Karin Wels (HRServices.MCS@tue.nl).

Are you inspired and would like to know more about working at TU/e? Please visit our career page.