[TYPES/announce] PhD, Postdoc and Technical Assistant openings in Formal Methods and Tools @ Uni Twente

Thu Mar 13 12:22:43 EDT 2008

We are looking for suitable candidates in various projects and on different
levels. For details on the projects see below.

PhD researchers (4 years) 
---------------
(note that these are fully paid positions, not studentships)

- 1 PhD on Graphs for the Abstract Interpretation of Languages (GRAIL)
- 1 PhD on Multi-Core Model Checking (MCMC)
- 1 PhD on Symbolic Translation of Stochastic Processes (STOP)

Postdoctoral researchers
------------------------

- 1 Postdoc (1 year) in Graphs for Software Language Definition (GRASLAND)
- 1 Postdoc (1.5 year) in INtegrated European Signalling System (INESS)
(possibly with an extension to 3 years)
- 1 Postdoc (3 years) in Quantitative System Properties in Model-Driven-Design
of Embedded Systems (QUASIMODO)

Technical assistants
--------------------

- 1 Technical Assistant (3 years) for the Laboratory on Interoperability of
Small Tools (LIST)

Deadline for all applications: 18 April 2008

Project descriptions
====================

GRAIL (PhD researcher, vacancy number 08/075)
-----

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., ensuring its correct functioning under
all circumstances. Reasons for this are, on 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 project 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.

For further information, please contact Arend Rensink rensink at cs.utwente.nl or
consult the full project description (http://fmt.cs.utwente.nl/grail)

MCMC (PhD researcher, vacancy number 08/076)
----

The goal of this project is to develop model checkers that exploit the
computing power of clusters of computers, GRIDs, multi-core machines, and their
heterogeneous combination. We aim at the development and understanding of new
distributed and parallel algorithms, and we want to build a high-quality
tool. We will consider branching and temporal logics, parity games, including
some quantitative extensions.

For further information, please contact Jaco van de Pol vdpol at cs.utwente.nl

STOP (PhD researcher, vacancy number 08/077)
----

The goal of this project is to integrate model checking techniques for
languages with rich data types, and languages with probabilistic, stochastic,
and timing information. The aim is to identify, study and implement model
transformations at the language level, in order to minimize state spaces even
before their generation, while preserving functional and quantitative
properties. Topics of interest are linearization, static analysis, abstraction,
and confluence reduction for languages with data and quantitative information.

For further information, please contact Jaco van de Pol vdpol at cs.utwente.nl or
Joost-Pieter Katoen katoen at cs.utwente.nl

GRASLAND (Postdoc, vacancy number 08/078)
--------

In the context of the MDA (Model Driven Architecture) methodology for designing
maintainable software systems, model transformation is a central
concept. Models are used to describe the system in all phases of development
and on various levels of abstraction; they are specified in diverse (modelling
and programming) software languages (SLs). Model transformations typically
introduce concrete, implementation specific details.

Such transformations are intended to be correctness preserving: they should not
introduce errors or essential changes. This, however, can be guaranteed only if
the meaning of the SLs involved is defined with sufficient
precision. Unfortunately, this is often lacking: many SLs have a well-defined
syntax but only an informal semantics. A primary reason for this is that MDA
does not include a general method for easily and consistently defining the
subtler aspects of SLs, such as their semantics.

The purpose of this project is to define a meta-language in which all aspects
of SLs, besides their concrete syntax, can be defined in a consistent
manner. As a common formal foundation of this meta-language we propose graphs
and graph transformations, which we believe to be powerful enough to capture
all relevant SL aspects. This meta-language will enable us to provide semantic
definitions of the source and target SLs involved in a given model
transformation on a compatible basis; this in turn will enable us to precisely
formulate and check the requirement of correctness preservation. We believe
these abilities to be essential in realizing the full potential of MDA.

For further information, please contact Arend Rensink rensink at cs.utwente.nl or
consult the full project description (http://trese.cs.utwente.nl/grasland).

INESS (Postdoc, vacancy number 08/079)
-----

Today there are over 20 rail signalling and speed-control systems operating in
Europe, which are incompatible with each other. This complexity leads to
additional costs and increased risk of breakdowns. Promoted by the European
Commission and driven by the need for interoperability and harmonisation of
safety, the European Rail Traffic Management System (ERTMS) aims to remedy this
lack of unification in the signalling and speed control.

The INESS project aims at contributing to the above mentioned European
initiatives by defining and developing specifications for a new generation of
interoperable interlocking systems suitable to be integrated in the ERTMS
system to ease the migration. This will enhance the standardisation process and
therefore, help increasing the competitiveness of the railway transport.

In Twente, you will work on formal specification and validation of requirements
on railway signalling systems, and on verifying and testing their design. We
promise you a very interesting case study.

For further information, please contact Jaco van de Pol vdpol at cs.utwente.nl

QUASIMODO (Postdoc, vacancy number 08/080)
---------

Quasimodo is a European research project funded by the European Commission
under the IST framework programme 7 for Information and Communication
Technology, ICT. Partners are found in Denmark, Germany, France and The
Netherlands.

Embedded Systems is the designation for intelligent and smart computer
controlled mechanical devices. Today - and even more so in the near future -
computers are built into everyday appliances existing anywhere in our
surroundings. Examples include laundry-machines, climate control systems, cars,
and satellites.  It is the combination of mechanics, computer electronic, and
an enormous amount of software that makes the devices intelligent, but at the
same time so extremely complex that they are difficult to develop.

The main goal of Quasimodo is to develop new techniques and tools for
model-driven design, analysis, testing and code-generation for advanced
embedded systems while ensuring quantitative bounds on resource consumption is
a central problem. Within this goal, the effort of the University of Twente
will be towards various aspects, such as model checking, controller synthesis,
and testing. The postdoc is expected to contribute to the research in one or
more of these fields, in close cooperation with the ESI (Embedded Systems
Institute) and several industrial partners in the Quasimodo project.

For further information, please contact Rom Langerak langerak at cs.utwente.nl or
consult the project web site, http://www.quasimodo.aau.dk.

LIST (Technical Assistant, vacancy number 08/081)
----

A "small tool" is the type of software tool typically created in the course of
a research project, as carried out by a single PhD student. Such tools have a
small basis for maintenance and more often than not "die" with the end of the
project, without having had a chance of being embedded or tested in a larger,
systems engineering context. It is a common observation, recently repeated in
the Dutch 3TU computer science assessment, that policy and infrastructure are
missing to change this situation.

In this project, we propose to set up a framework for the improved integration
and maintenance of small tools in the area of formal methods, with the aim of
offering such tools better usability, better accessibility and a longer
lifespan. This will provide these tools with more chance of proving themselves
in practice, and thus help to valorise the effort that went into their
creation. The project will be carried out in cooperation with similar efforts
at the Technical Universities of Eindhoven and Delft.

The task of the technical assistant will initially consist of forging concrete
interoperability links between specific (existing) tools. Using the expertise
thus built up, the next step is to generalise from this, and to identify and
bring together the necessary elements for an integration and maintenance
framework.

For further information, please contact Arend Rensink rensink at cs.utwente.nl

Profile
=======

To qualify for any of the PhD positions, you must have an MSc or comparable
degree and a good background in formal methods. Expertise in the specific area
of the project is considered an advantage. Good English speaking and writing
skills are demanded, as well as the willingness to learn Dutch. The candidates
will enrol in the PhD programme of the Dutch Research School for Programming
Research and Algorithmics (IPA).

To qualify for any of the postdoc positions, you must have a PhD degree in a
relevant area of formal methods. Good English speaking and writing skills are
demanded, as well as the willingness to learn Dutch.

Offer
=====

A PhD researchership in the Netherlands is a fully paid position, for a period
of 4 years. The candidate will receive a gross salary starting at   2000 per
month (first year) and reaching   2558 per month (final year), plus an 8%
holiday allowance and other benefits.

The postdoc positions are for 1 year (GRASLAND), 1.5 years (INESS) and 3 years
(QUASIMODO), respectively. Your starting salary is   2802 per month, but may be
higher depending on experience, plus an 8% holiday allowance and other
benefits.

The technical assistant position is for 3 years. Your starting salary is   2802
per month, but may be higher depending on experience, plus an 8% holiday
allowance and other benefits.

To qualify for the technical assistant position, you must have a BSc degree
from a university or polytechnic, practical programming skills, as well as the
ability to grasp and abstract problems, and to understand the principles behind
formal methods tools. Good English speaking and writing skills are demanded, as
well as the willingness to learn Dutch. Experience with software development
and maintenance is an advantage.

Application
===========

You are invited to send your application together with:

- 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 (in case of a PhD or TA position) or PhD thesis (in case of a
postdoc position).
- Letters of recommendation or references of at least two scientific staff
members.

Letters should be sent by email to the relevant contact person, mentioning the
vacancy number in the header, with a cc to Ms. Joke Lammerink
jlammeri at cs.utwente.nl :

- GRAIL PhD researcher: rensink at cs.utwente.nl, vacancy number 08/075
- MCMC PhD researcher: vdpol at cs.utwente.nl, vacancy number 08/076
- STOP PhD researcher: vdpol at cs.utwente.nl and katoen at cs.utwente.nl, vacancy
number 08/077
- GRASLAND postdoc: rensink at cs.utwente.nl, vacancy number 08/078
- INESS postdoc: vdpol at cs.utwente.nl, vacancy number 08/079
- QUASIMODO postdoc: langerak at cs.utwente.nl, vacancy number 08/080
- LIST technical assistant: rensink at cs.utwente.nl, vacancy number 08/081

All applications must be received ** at or before 18 April 2008 **