[TYPES/announce] Post-doctoral position on verification for domain-specific languages

[Stephan Merz]

Post-doctoral position: Verification for domain-specific languages

Applications are invited for a post-doctoral fellowship on the modeling
and verification of domain-specific languages in the MOSEL team at LORIA
(http://www.loria.fr/equipes/mosel/).

The research will be carried out within the project VeriTLA+ (A
Verification Environment for TLA+ Applied to Service Descriptions,
http://wiki.loria.fr/wiki/VeriTLA). Within this project, we aim to model
domain-specific languages in the specification language TLA+
(http://research.microsoft.com/users/lamport/tla/tla.html) and to
develop verification techniques for programs written in DSLs
against (domain-specific) high-level correctness properties. Because the
properties are fixed and the expressiveness of DSLs is limited, we hope
to obtain a significant degree of automation. These techniques will be
validated for DSLs for communication services
(http://phoenix.labri.fr/research/commServices/) and for schedulers in
operating systems (http://www.emn.fr/x-info/bossa/). The post-doctoral
researcher will interact intensively with the designers of these
languages. TLA+ is currently supported by a mature model checker,
a proof environment is being developed in a companion project.

Candidates must hold a PhD and should have demonstrated research
interest in formal methods and formal reasoning. They should preferably
have experience with interactive proof assistants. (Prior knowledge of
TLA+ is not a prerequisite.) The fellowship gives an opportunity to
carry out research in collaboration with four INRIA projects in France
and with several international partners. The appointment is for one
year, the salary is 2150 euros per month. The position must be filled by
December 1, 2006.

Applications, including a curriculum vitae, references, and a short
description of research interests should be sent by email to
Stephan.Merz at loria.fr, who is also available for informal inquiries and
discussions about the position.





-------------- next part --------------
A non-text attachment was scrubbed...
Name: Stephan.Merz.vcf
Type: text/x-vcard
Size: 325 bytes
Desc: not available
Url : http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20061005/dc02ab51/Stephan.Merz.bin