[TYPES/announce] PhD position at the University of Twente on Graph-Based Abstract Interpretation

[Arend Rensink]

To carry out the recently awarded Dutch (NWO) research project entitled "Graphs
for Abstract Interpretation of Languages" (GRAIL), we are offering a position
for a PhD student (fully funded) for a period of four years.

- Deadline for applications: August 30, 2007
- Project start date: October 1, 2007, or as soon thereafter as possible

The Context
===========

The project takes place at the Formal Methods and Tools chair of the University
of Twente. This chair is part of the Department of Computer Science, one of the
largest academic departments for computer science in the etherlands. Project
leader is Dr. Arend Rensink.

The Project: Graphs for Abstract Interpretation of Languages (GRAIL)
====================================================================

As more and more systems in our everyday environment contain major software
parts, and we are depending on such systems more and more (we are counting on
them), the importance of the dependability of the embedded software is
increasing. Unfortunately, there are still very few generally applicable
methods for software verification, i.e., the ensurance of its correct
functioning under all circumstances. Reasons for this are, one the one hand,
the degree of expertise necessary for existing verification methods, and on the
other, their poor embedding in the average software development trajectory. An
important practical objection is, moreover, that current verification methods
typically assume the existence of a sufficiently detailed and precise model of
system behaviour. In practice such models hardly ever exist, and the time and
expertise to construct them is missing. Examples of methods that are being used
widely in practice are therefore typing and testing, neither of which
necessarily depends on the pre-existence of models.

In this procect we investigate a new way of automatically verifying software on
the basis of code, without assuming a predefined model. The technique used is
static analysis, a general principle that encompasses typing; the new aspect is
the use of graph transformations to capture the effect of the software. Graphs
offer a natural model for the behaviour of dynamic software systems, and at the
same time offer the basis for a generic form of static analysis, which can be
driven by the properties to be verified.

The full project proposal can be found at
http://www.cs.utwente.nl/~rensink/projects/grail.pdf

The position
============

You should have a MSc or equivalent degree in computer science or a closely
related area, or be able to show that you will receive the degree this year
(2007). Familiarity with formal verification, abstract interpretation and/or
and graph transformations is considered an advantage. You are expected to
cooperate in an internationally oriented research environment. Good English
speaking and writing skills are demanded, as well as the willingness to learn
Dutch. You will enroll in the PhD programme of the Dutch Institute for
Programming Research and Algorithmics (IPA).

The selected candidate will be appointed for a period of 4 years with a gross
salary starting at around EUR 1950 per month (first year) and reaching EUR 2500
per month (final year), plus an 8% holiday allowance and other benefits.

Your Application
================

You can obtain further information about the positions by enquiring from:

  Dr.ir. Arend Rensink,
  mailto:rensink at cs.utwente.nl,
  tel: +31 (0)53 489 4862
  fax: +31 (0)53 489 3247

If you are interested, please send an application by email to the above
address, including:

- A cover letter stating your *specific* interest in the position, indicating
also your motivation and qualifications for joining the project. (In the
absence of such a cover letter your application will be rejected without
notification.)

- A full curriculum vitae, including the subject and supervisor of your
graduate thesis.

- Letters of recommendation or references of at least two scientific staff
members.

All applications must be received ** at or before 30 August 2007 **