[Caml-list] research engineer / post-doc opening

[Damien Doligez <damien.doligez@inria.fr>]

This is an announcement for a job opening that involves lots of
programming in OCaml...

-- Damien


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@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/