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.

• You have a strong background in interactive theorem proving and/or formal methods for (software) verification.
• You have, or are about to acquire a MSc degree with excellent grades, ideally on a topic related to theorem proving or formal methods.
• You are an enthusiastic and highly motivated researcher, curious to learn new methods and put them to use.
• You are proficient in English. Dutch is not required, but there will be an opportunity to learn.

• As a PhD student at UT, you will be appointed to a full-time position for four years, with a qualifier in the first year, within a very stimulating and exciting scientific environment;
• The University offers a dynamic ecosystem with enthusiastic colleagues;
• Your salary and associated conditions are in accordance with the collective labour agreement for Dutch universities (CAO-NU);
• You will receive a gross monthly salary ranging from € 2.541,- (first year) to € 3.247,- (fourth year);
• There are excellent benefits including a holiday allowance of 8% of the gross annual salary, an end-of-year bonus of 8.3%, and a solid pension scheme;
• The flexibility to work (partially) from home;
• A minimum of 232 leave hours in case of full-time employment based on a formal workweek of 38 hours. A full-time employment in practice means 40 hours a week, therefore resulting in 96 extra leave hours on an annual basis.
• Free access to sports facilities on campus
• A family-friendly institution that offers parental leave (both paid and unpaid);
• You will have a training programme as part of the Twente Graduate School where you and your supervisors will determine a plan for a suitable education and supervision;
• We encourage a high degree of responsibility and independence, while collaborating with close colleagues, researchers and other staff.

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.