PhD on GPU accelerated symbolic reasoning about software systems

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.

Job Requirements

• 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.

Conditions of Employment

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.

Information

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.

Application

We invite you to submit a complete application by using the apply button. The application should include a:

• Cover letter in which you describe your motivation and qualifications for the position.
• Curriculum vitae, including a list of your publications and the contact information of three references.
• Copies of relevant BSc and MSc diplomas and transcript of records.
• A copy or link to your master thesis if available. In case you are currently writing your master thesis, a short description of the project.

We look forward to receiving your application and will screen it as soon as possible. The vacancy will remain open until the position is filled.

Reference number: 2025/282