[Jmlspecs-interest] PhD position on Program Analysis for LLVM-IR and all its source languages @ University of Twente, Netherlands

[Huisman, M. (UT-EEMCS) <m.h...@ut...>]

PhD position on Program Analysis for LLVM-IR and all its source languages
University of Twente, Netherlands
To apply, visit: https://utwentecareers.nl/en/vacancies/1320/phd-position-on-program-analysis-for-llvm-ir-and-all-its-source-languages/

* The project *

Formal verification can play an important role to ensure that software is free of errors. To enable formal verification for many different programming languages, we will develop a deductive verifier for an intermediate language, and then build deductive verifiers for many different source languages on top of this.

With the omnipresence of software, our lives and income depend crucially on the quality of software: software failures can cause planes to crash, emergency service to be unreachable, and companies to lose millions of dollars (because of missed business opportunities, but also due to reputation damage). Therefore, software developers are urgently looking for techniques that can help them to improve the quality of their software. Formal verification techniques that allow one to prove that software will never reach an erroneous state can play an essential role in this. However, to use this in an industrial setting, we need to make sure that the verification technology can be used in combination with the newest programming language technology. Deductive program verification is a formal verification technique that works directly at the code level, and non-trivial case studies have shown its potential. However, for its widespread use, we need tool support for many different programming languages, which requires a large amount of engineering.

Therefore, in this project, you will be working on a different approach. Rather than building a deductive program verifier for each programming language, you will develop deductive program verification technology for the widely-used intermediate representation language LLVM-IR. You can use deductive verification for any programming language that compiles into the LLVM-IR format.

In addition, you will define a generic specification format to write the program specifications, which is then automatically compiled into a specified LLVM-IR program, and which can be verified. Finally, you will also develop techniques to give feedback on failed verification attempts at the level of the source program, rather than asking the developer to study the generated LLVM-IR code. Throughout the project, you will evaluate the verification technology on various industrial case studies, including applications that use multiple programming languages, that are all targeting the LLVM-IR format.

You will work on this project in close collaboration with the members of the VerCors team, who are working on the VerCors program verifier (see utwente.nl/vercors/).

* Your profile *

- You are an enthusiastic and highly motivated researcher.
- You have, or will shortly, acquire a master's degree in the field of Computer Science, or comparable.
- You have a demonstrable interest in formal specification and verification and an affinity with tool development.
- You have a creative mentality and excellent analytical and communication skills.
- You have a good team spirit and like to work in an interdisciplinary and internationally oriented environment.
- You are proficient in English.

* Our offer *

- As a PhD candidate 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;
- You will be a member of the Formal Methods and Tools research group, a strong research group on formal verification, with an open and welcoming atmosphere;
- 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. 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.

* Information and application *

Are you interested in this position? Please send your application via the 'Apply now' button below before August 31, 2023, and include:

- A cover letter (maximum 2 pages A4), emphasizing your motivation to apply for this specific position.
- A Curriculum Vitae, including a list of all courses attended and grades obtained, and, if applicable, a list of publications and references.
- The names of 2 or 3 people who can be contacted for additional information about you.

For more information regarding this position, you are welcome to contact prof.dr. Marieke Huisman, m.h...@ut...<mailto:m.h...@ut...>

Interviews are scheduled in September.

To apply, visit https://utwentecareers.nl/en/vacancies/1320/phd-position-on-program-analysis-for-llvm-ir-and-all-its-source-languages/