PhD position on automated verification of concurrent software (Mercedes project)

Where to apply

In the Formal Methods and Tools (FMT) research group, formal techniques and tools are developed and used as a means to support the development of software. Formal methods are mathematical techniques for the construction and analysis of software systems. Our central goal is to increase the reliability of the software that we rely on, as individuals and as society. We primarily target complex concurrent ICT systems, embedded in a technological context or in a distributed environment.

The FMT group is part of the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) at the University of Twente. The FMT group also participates in the research institute CTIT.

 

We are looking for an excellent candidate for a PhD project on automated verification of concurrent software. The PhD position (for 4 years) is part of the Mercedes project on Maximal Reliability of Concurrent and Distributed Software.

University of Twente

Group: Formal Methods and Tools

Contact: Prof.dr. Marieke Huisman (m.huisman@utwente.nl)

Project webpage: http://fmt.ewi.utwente.nl/research/projects/Mercedes/

 

The challenge

You will be working on the Mercedes project, a 1,5 million euro personal grant for Marieke Huisman, funded by NWO.

 

Goal of the Mercedes project is to develop techniques to ensure the maximal reliability of concurrent and distributed software. In earlier projects, we started working on the development of a tool set for the verification of concurrent programs, called VerCors. The VerCors tool set uses deductive program verification, i.e., the desired program properties are written in a pre-postcondition style (using a form of separation logic). To make verification succeed, often a large number of auxiliary annotations have to be added in the code. The goal of this PhD project is to make the verification process faster, by developing techniques to automatically generate the necessary additional annotations. This project will involve defining new combinations of existing techniques such as static analysis, heuristic search, and possibly also some form of learning.

 

All results of the Mercedes project will be integrated in the VerCors tool set for verification of concurrent software, which is a result of Marieke Huismans earlier ERC project on verification of concurrent software.

 

For more information about the concrete project, please contact Marieke Huisman.

 

Our offer

The University of Twente offers excellent working conditions, an exciting scientific environment, and a green and lively campus. We offer:

  • A PhD position for four years (38 hrs/week).
  • A stimulating scientific environment
  • Full status as an employee at the University of Twente, including pension and health care benefits.
  • Gross salary PhD student: ranging from 2.325,00 (1st year) to 2.972,00 (4th year) per month, plus holiday allowance (8%) and end-of-year bonus (8.3%).
  • Excellent facilities for professional and personal development.
  • Good secondary conditions, in accordance with the collective labour agreement CAO-NU for Dutch universities.
  • A green and lively campus, with lots of sports facilities and other activities.

Starting date of the position: as soon as possible, to be discussed.

 

The PhD students will be members of the Twente Graduate School in the research programme 'Dependable and Secure Computing'. The research programme offers advanced courses to deepen your scientific knowledge in preparation to your future career (within or outside academia). We provide our PhD students with excellent opportunities to broaden their personal knowledge and to professionalise their academic skills. Participation in national and/or international summer schools and workshops, and visits to other prestigious research institutes and universities can be part of this programme.

 

Your profile

We are looking for enthusiastic students that hold a MSc degree in Computer Science (or equivalent). The candidates should have a thorough theoretical background, a demonstrable interest in program verification and some knowledge about multithreaded programming (in Java/C/C++).

As a research outcome we expect publications, (prototype) tools and a PhD thesis.

 

Your application should consist of:

  • a cover letter (explaining your specific interest and qualifications);
  • a full Curriculum Vitae;
  • a list of all courses + marks and a short description of your MSc thesis;
  • references (contact information) of two scientific staff members.

Deadline: as soon as possible, or until the positions are filled.

 

You can submit your application by sending an email to Marieke Huisman: m.huisman@utwente.nl.

 

Further information: