VeriTLA Postdoc

Un article de Loria Wiki.

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.

The research will be carried out within the project VeriTLA+ (A Verification Environment for TLA+ Applied to Service Descriptions). Within this project, we aim to model domain-specific languages in the specification language TLA+ and to develop strategies for the verification of 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 and for schedulers in operating systems. 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. Experience with using interactive proof assistants is particularly welcome. (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 several international partners. The appointment is for one year, the salary is 2150 euros per month. The position must be filled before December 1, 2006.

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