[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
PhD position on Program Analysis for LLVM-IR and all its source languages
University of Twente, Netherlands
To apply, visit:
https://urldefense.com/v3/__https://utwentecareers.nl/en/vacancies/1320/phd-position-on-program-analysis-for-llvm-ir-and-all-its-source-languages/__;!!IBzWLUs!W2RbE1oBoSXEP40yPEm-d9IC4TwHFUT0zPH9toyjMaBieu5yIAHl3CkMJzBzDui5CMbEbIWrE6EavZQu7wQ4gVmYkHPURoywgJe9$
* 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.huis...@utwente.nl<mailto:m.huis...@utwente.nl>
Interviews are scheduled in September.
To apply, visit
https://urldefense.com/v3/__https://utwentecareers.nl/en/vacancies/1320/phd-position-on-program-analysis-for-llvm-ir-and-all-its-source-languages/__;!!IBzWLUs!W2RbE1oBoSXEP40yPEm-d9IC4TwHFUT0zPH9toyjMaBieu5yIAHl3CkMJzBzDui5CMbEbIWrE6EavZQu7wQ4gVmYkHPURoywgJe9$
