[TYPES/announce] post-doc position at MSR-INRIA centre, Paris, France

[Stephan Merz]

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

The Microsoft Research-INRIA Joint Centre is offering a 2-year
position for a post-doctoral researcher to contribute to a proof development
environment for TLA+ developed in the Tools for Proofs project (see
http://www.msr-inria.inria.fr).

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, temporal logic, and a module system.
TLA+ and its tools have been used in industry for over a decade.  More
recently, we have extended TLA+ to include hierarchically structured
formal proofs that are independent of any proof checker.  We have
released several versions of the TLAPS proof checker
(http://msr-inria.inria.fr/~doligez/tlaps/) and integrated it into the
TLA+ Toolbox, an IDE for the TLA+ tools
(http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html).

TLAPS and the Toolbox support the top-down development of proofs and
the checking of individual proof steps independently of the rest of
the proof.  This helps users focus on the part of the proof they are
working on.  Although still lacking important features, TLAPS is
already a powerful tool and has been used for a few verification
projects, including a proof of the safety properties of a Byzantine-fault
tolerant consensus algorithm
(http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html).

TLAPS consists of the Proof Manager (PM, an interpreter for the
proof language that computes the proof obligations corresponding to
each proof step) and an extensible list of backend provers. Current backends
include the tableau prover Zenon, an encoding of TLA+ as an object logic
in the Isabelle proof assistant, and a generic backend for SMT solvers.
When possible, we expect backend provers to produce a detailed proof that
is then checked by Isabelle.  In this way, we can obtain high assurance
of correctness as well as satisfactory automation.

The current version of the PM handles only the "action" part of TLA+:
first-order formulas with primed and unprimed variables, where a
variable v is considered to be unrelated to its primed version v'.
This allows us to translate non-temporal proof obligations to standard
first-order logic, without the overhead associated with an encoding of
temporal logic into first-order logic.

Description of the activity of the post-doc
===========================================

You will work with other members of the project, including Leslie
Lamport, Damien Doligez, and Stephan Merz, on the extension of the
TLA+ proof language to temporal operators.  This extension poses
interesting conceptual and practical problems.  In particular, the new
translation must smoothly extend the existing one since temporal proof
steps rely on action-level subproofs.  You will have the primary
responsibility for designing and implementing algorithms to generate
corresponding proof obligations.

As time permits and depending on your interests, you will have the
opportunity to contribute to further improving the proof checker.
This may include:
- adding support for certain TLA+ features that are not yet handled by
  the PM, such as recursive operator definitions and elaborate patterns
  for variable bindings;
- finding what improvements are needed by verifying real examples, perhaps
  including liveness of the aforementioned consensus algorithm;
- integrating new backends to improve the automation of proofs;
- adding validation of proofs by backends whose proofs are not
  now checked.

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

You should have a solid knowledge of logic and set theory as well as
good implementation skills related to symbolic theorem proving.  Of
particular relevance are parsing and compilation techniques.  Our
tools are mainly implemented in OCaml.  Experience with temporal and
modal logics, Isabelle, Java or Eclipse would be a plus.

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 Microsoft Research-INRIA Joint Centre is located on the Campus of
INRIA Saclay south of Paris, near the Le Guichet RER station.

Starting date
=============

The normal starting date of the contract would be September 2012,
but we can arrange for an extremely well-qualified candidate to
start sooner.

Contact
=======

Candidates should send a resume and the name and e-mail addresses of
one or two references to Damien Doligez <damien.doligez at inria.fr>.
The deadline for application is April 15, 2012.

This announcement is available at
http://www.msr-inria.inria.fr/Members/doligez/post-doc-position-2012/view