The department of Computer Science and Engineering provides a strong, international, and dynamic research environment with about 75 faculty and 75 PhD students. For more information, see http://www.chalmers.se/cse/EN/.

The two PhD students will join a world-leading team of researchers in the field of formal methods. They will participate in two EU projects, HATS (www.hats-project.eu) and CHARTER, with ca. 20 international academic and industrial partners.

The HATS (Highly Adaptable and Trustworthy Software Using Formal Methods) project addresses challenges arising from the increasing need to design and maintain long-living trustworthy software systems. These software systems, used for e.g. in e-commerce or e-government, pose requirements on maintenance and reusability of components for which current software development approaches are insufficient. Development methods must take into consideration the need for high adaptability of these systems in terms of features and deployment platforms. They must also provide means to give and enforce guarantees like functional correctness or adherence to security policies. To this end, and to achieve automation for static and runtime analysis of consistency properties or trustworthy code generation, a rigorous formal foundation is necessary. Specific goals for the PhD position within the HATS project are:

• contribute to the design of an abstract behavioural, executable and object-oriented specification language (ABS) parametric with respect to deployment issues
• development of a program logic and calculus for ABS with efficient symbolic execution
• test-case generation algorithms based on ABS models that are able to cope with non-determinism resulting from concurrency issues on different deployment platforms
• development of algorithms and tools supporting visualisation and debugging of ABS models
• refinement and reuse of verification results with respect to changes in requirements and implementations of software components

The CHARTER project is closely related to HATS, but with a focus on embedded software in real-time environments as for example used in avionics. The ultimate goal is to ease and accelerate the certification of critical embedded systems by combining real-time Java, model-driven development, rule-based compilation and formal verification. Specific goals for the PhD position within the CHARTER project are:

• formalisation of floating point arithmetic together with the development of an efficient, highly automatised symbolic reasoner
• verification-driven test-case generation satisfying criteria required for safety critical software in order to be certified; the developed test generation facilities will be used to generate test cases for the Java Safety Critical Libraries
• generation of gap-free certificates from verification proofs that can be validated by proof checkers

Details about Employment

PhD student positions are limited to five years and will then normally include 20 per cent departmental work, mostly teaching duties. Salary for the position is as specified in Chalmers general agreement for PhD student positions, currently around 23,000 SEK a month before tax.

The positions are intended to start in Spring 2009.

Applicants must have a degree in Computing Science or in a related subject with a strong Computing Science component. They must also have a strong, documented interest in doing research. The ideal student for the project will have strong background in formal methods (esp. logics or formal specification languages) and software engineering. You may even apply if you have not yet completed your degree, but expect to do so before the position starts. In order to improve gender balance, Chalmers welcomes in particular applications from female candidates.

Knowledge of Swedish is not a prerequisite for application. English is our working language for research. Both Swedish and English are used in undergraduate courses. Half of our researchers and PhD students are native Swedes; the rest come from more than 30 different countries.

You MUST include or e-mail letters of recommendation: we typically get a large number of applications, and it is simply not feasible for us to request individual letters!

In contrast to the general instructions above, there is no need for copies of degrees and certificates to be attested, if submitting the application electronically.

It is essential that the application includes all relevant work such as theses and articles that you have authored or co-authored.

For further information contact:

Research level:

Professor Reiner Hähnle, e-mail reiner@chalmers.se

Senior Lecturer Wolfgang Ahrendt, e-mail ahrendt@chalmers.se

Department level:

Graduate studies director Jan Jonsson, e-mail janjo@chalmers.se

Vice Head of Department, Graduate Education: Professor Reiner Hähnle

• SACO: Jan Lindér
• ST: Marie Wenander
• SEKO: Ralf Berndtsson

All reachable via Chalmers exchange: +46 31 772 10 00