PhD position on Verification of Efficient and Secure Parallel Algorithms

Are you interested in Theorem Proving? And want to use your skills to make software more secure? Then this position may be for you!

To fully exploit the potential of modern hardware, parallel algorithms are required. However, these are also prone to new types of hard-to-find bugs, like data races. In critical software, these frequently cause costly incidents or open the door for hackers.

In this project you will apply a theorem prover to show the correctness of parallel software. The challenge is two-fold: first, theoretical models of concurrency have to be formalized in the theorem prover, and, second, techniques to scale them to real software have to be explored.

The initial focus will be on shared-memory architectures (Multicore CPUs, GPUs), but targetting message-passing is also an option.

You will be supervised by Peter Lammich, who is an expert in the Isabelle Theorem Prover, and has scaled (sequential) verification techniques to large and complex software. As member of the FMT group, you will have the opportunity to be a part of cutting-edge research on verification of concurrent software.

Are you interested in this position? Please send your application via the 'Apply now' button below before May 10th, and include:

• A curriculum vitae
• A copy of (or link to) your best work in the field of formal methods, with a short summary. This could be a paper, thesis, research project, etc. For a group work, explain your contribution. If you don't have such work: include a motivation letter that explains how this PhD position suits you and your skills (max. 500 words).
• An academic transcript of your bachelor and master education, including grades.

For more information regarding this position, you are welcome to contact Peter Lammich [email protected]

You will work in the Formal Methods Group (FMT) of the Electrical Engineering, Mathematics and Computer Science faculty (EEMCS).
The mission of FMT is to develop mathematical methods, high-performance data structures and algorithms, and suitable programming languages for the design of reliable software- and data-intensive control systems.
We focus on modelling, synthesis, analysis, prediction and maintenance of their functional, structural and quantitative aspects. We aim to understand safety, reliability, performance, energy usage of complex systems and the risks and costs associated to their architecture, design, operation and maintenance.
Our mission builds on extensive experience in concurrency theory, static analysis, theorem proving, language design, model checking and term/graph rewriting.

Our focus areas are:

• Quantitative modelling and analysis for cyber-physical and socio-technical systems;
• Program design and verification for (concurrent) software;
• High-performance algorithms and data structures for model checking and model transformation.

The faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) uses mathematics, electronics and computer technology to contribute to the development of Information and Communication Technology (ICT). With ICT present in almost every device and product we use nowadays, we embrace our role as contributors to a broad range of societal activities and as pioneers of tomorrow's digital society. As part of a people-first tech university that aims to shape society, individuals and connections, our faculty works together intensively with industrial partners and researchers in the Netherlands and abroad, and conducts extensive research for external commissioning parties and funders. Our research has a high profile both in the Netherlands and internationally. It has been accommodated in three multidisciplinary UT research institutes: Mesa+ Institute, TechMed Centre and Digital Society Institute.