[TYPES/announce] opening for a research engineer (post-doctoral) position at MSR-INRIA centre

[Stephan Merz]

The following announcement should be of interest to members of the TYPES community working on proof assistants and formal verification, and I would be grateful if it could be distributed on the list.

--------------------------------------------------------------------------------------------

Research team: Tools for Proofs, MSR-INRIA Joint Centre
=======================================================

The Microsoft Research-INRIA Joint Centre is offering a 14-month position for a research engineer to contribute to the ADN4SE project. We hope the position will be extended to 18 months, but are not yet sure this will be possible.

The engineer will contribute to extending the TLA+ Proof System (TLAPS, http://msr-inria.com/projects/tools-for-proofs) and will assist domain experts in applying TLAPS for proving fundamental properties of PharOS, a real-time operating system.


Research Context
================

TLA+ is a language for specifying and reasoning about systems, including concurrent and distributed systems.  It is based on first-order logic, set theory, and temporal logic. TLA+ and its tools have been used in industry for over a decade.  More recently, we have extended TLA+ by a language for writing structured formal proofs and have developed TLAPS, a proof checker that contains an interpreter for the proof language and integrates different back-end provers. TLAPS is integrated into the TLA+ Toolbox, an IDE for TLA+ (http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).

Although it is still under active development, TLAPS is already quite powerful and has been used for a few verification projects, in particular in the realm of distributed algorithms (e.g., http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html).

The current version of TLAPS handles the "action" part of TLA+: first-order formulas with primed and unprimed variables that represent the values of a variable before and after a transition. It also supports the propositional fragment of temporal logic. This fragment is enough for proving safety properties (invariants and step simulation). We are currently refactoring the code base and preparing support for full temporal logic of TLA+, which will allow us to prove liveness and refinement properties.


Description of the activity of the research engineer
====================================================

The research engineer (post-doctoral) position is funded by the PIA ADN4SE project (http://www.systematic-paris-region.org/en/projets/adn4se) that develops a real-time operating system and development tools for embedded systems based on PharOS. The system aims at providing certifiable correctness and performance guarantees, and fundamental properties of the operating system, such as determinacy, are formally verified using the TLA+ notation and tools.

Your work will make a key contribution to this verification effort. In particular, you will work with members of the TLA+ project at the Microsoft Research - INRIA Joint Centre, including Damien Doligez, Leslie Lamport, and Stephan Merz on extending the TLA+ Proof System and its libraries. You will also work with the project partners of ADN4SE, and in particular members of CEA List, on modeling the protocols subject to verification and on carrying out the proofs. Your contributions will be conceptual, by identifying theories and patterns that underly the verification of the operating system, and practical, by implementing formal libraries and software in order to carry out the verification task.

You will also have the opportunity to contribute to further improving the proof checker, for example by adding support for certain TLA+ features that are not yet handled by TLAPS, integrating new back-end provers, or extending the capabilities for proof validation.


Skills and profile of the candidate
===================================

You should hold a PhD in computer science and have solid knowledge of mathematical logic as well as implementation skills related to symbolic theorem proving. Our tools are mainly implemented in OCaml. Some basic familiarity with concepts of real-time systems is a plus. Experience with temporal and modal logics, with interactive theorem provers or with Eclipse could be valuable.

Working on the project provides the opportunity to learn about the issues of using verification in practice, and it has in the past and may continue in the future to produce published research.  However, the main focus is on practical applications and on the implementation of components of our tool chain that are missing or need improvement.

Given the geographical distribution of the members of the team, we highly value a good balance between the ability to work in a team and the capacity to propose initiatives.

Location
========

The research engineer will be based at the INRIA research center in Nancy (http://www.inria.fr/en/centre/nancy). Located in the North-East of France, Nancy is a university town whose metropolitan area has about 400,000 inhabitants. It is 1-1/2 hours from Paris by TGV.


Contact
=======

Candidates should send a resume and the names and e-mail addresses of two references to Damien Doligez <damien.doligez at inria.fr>, preferably by September 22, 2014.

We intend to hire the research engineer by November 2014, although the exact date is negotiable.

This announcement is available at http://www.msr-inria.com/open_positions/research-engineer-position-on-tla-tools/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 1898 bytes
Desc: not available
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140910/6603ad85/attachment-0001.p7s>