[TYPES/announce] PhD and Post Doc position on ERC project Verifcation of Concurrent Data Structures (U. Twente, Netherlands)

[Marieke Huisman]

The research group
    Formal Methods and Tools
at the
    University of Twente
    (Enschede - The Netherlands)
is looking for a
    PhD researcher (4 years)
and a
    post doc researcher (3 years),
to work on the 5 year research project

    VerCors (Verification of Concurrent Data Structures),

funded by the European Research Council.

The PhD student will work in particular on:
   The specification and Verification of Concurrent Data Structures
   with different Locking Policies

The post doc researcher will work in particular on:
   User-friendly specification and automated verification of
   concurrent data structures


Our research:
-------------

Goal of the VerCors project is to develop a general specification and
verification technique for multithreaded software.

In earlier work, we developed a variant of permission-based separation
logic that is particularly suited to reason about multithreaded Java
programs with dynamic thread creation and termination, and reentrant
locks. Expressiveness of this logic will be extended, to specify and
verify different concurrent data structures.

The PhD student will work on the parametrisation of the verification
logic over the locking policy, so that a high-level specification of the
behaviour of a data structure can be reused for different
implementations. Thus the implementation of a concurrent data structure
can be changed, without affecting correctness of the applications using
it. The developed technique will be applied on standard concurrency
libraries, such as java.concurrency.util.

The post doc will be actively involved in the whole project. In
addition, he or she is expected to work in particular on the following
topics:
- the development of an appropriate specification language, combining
readability à la JML and expressiveness related with concurrency as in
separation logic.
- the automated verification of proof obligations, by developing or
extending appropriate solvers for separation logic, and developing
ownership type-based techniques to prove the absence of aliasing
automatically.

All results of the VerCors will be integrated in a tool set that
generates and proves proof obligations automatically. It will be
validated on realistic case studies.

For more information about the project, see:
http://fmt.cs.utwente.nl/projects/VerCors/

We seek:
--------
A PhD student with an MSc degree in Computer Science (or an equivalent
qualification) and a post doc with a PhD degree in Computer Science (or
an equivalent qualification).
The candidate should be enthousiastic, and have a thorough theoretical
background, a demonstrable interest in program verification, and some
knowledge about multithreaded programming (in Java/C/C++).

We are looking for a researcher with an independent mind who is willing
to cooperate in our team. It is understood that he or she works on the
topics listed above.  Further we ask for good communicative and good
collaboration skills. Candidates should be prepared to prove their
English language skills.

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

Starting date of the position: as soon as possible after February 1, 2011.

We offer:
---------
- A PhD position for four years (38 hrs/week) and a post doc position
for three years (38 hrs/week)
- A stimulating scientific environment
- Gross salary for a PhD student ranging from E 2042 tot E 2612 (4th
yr) per month
- Post doc salary is dependent on experience and background, but will
minimally be EUR 2861 gross per month, plus benefits.
- Holiday allowance (8%), 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 Campus with lots of sports facilities

The PhD student will be a member of the Twente Graduate School in the
research programme 'Dependable and Secure Computing' under the
leadership of Prof Dr Jaco van de Pol. 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.

Further information:
--------------------
- FMT group: http://fmt.cs.utwente.nl/
- Dr. Marieke Huisman (Marieke.Huisman at ewi.utwente.nl)

Application:
------------
Please submit your application via http://www.utwente.nl/vacatures/en/
before December 15th, 2010. However, we strongly encourage interested
applicants to send in their applications as soon as possible.

Your application should consist of:

- a cover letter (explain your specific interest and qualifications);
- a full Curriculum Vitae,
  to apply for the PhD student position, this should include a list of
  all courses + marks, and a short description of your MSc thesis;
  to apply for the post doc position, this should include a list of
  all publications, and a short description of your PhD thesis;
- references (contact information) of two scientific staff members.