[TYPES/announce] research engineer (postdoc) position at MSR-Inria Joint Centre

[Stephan Merz]

Although the TLA+ language is set theoretic, the development of the TLA Proof System relies on concepts from type theory, and the position would therefore be of interest of readers of this list.

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

The Microsoft Research-INRIA Joint Centre is offering a 24-month position for a
research engineer to contribute to the design and further development of the
TLA+ Proof System (TLAPS, http://msr-inria.com/projects/tools-for-proofs).


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
more than 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 interfaces with different
back-end provers, including SMT solvers, the tableau prover Zenon that supports
set-theoretic constructions, and a declarative encoding of TLA+ set theory as
an object logic in the logical framework Isabelle. TLAPS is integrated into the
TLA+ Toolbox, an IDE for TLA+ (http://lamport.azurewebsites.net/tla/tla.html).

Although it is still under active development, TLAPS is already quite powerful
and has been used for several verification projects, in particular in the realm
of distributed algorithms (e.g., http://lamport.azurewebsites.net/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 have initiated a complete
rewrite of the code base, with the aim of providing support for module
instantiation and for the 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 for 24 months by the
Microsoft Research - Inria Joint Centre. You
will work together with the members of the TLA+ project, including Damien
Doligez, Leslie Lamport, and Stephan Merz on extending the TLA+ Proof System.
Your main objective will be to complete the rewrite of the existing version of
TLAPS so that it can be released to users of the prover. You will also be able
to work on extensions of existing functionality, including the following items:

- Module instantiation. The TLA+ language contains a module system, and modules
 can have constant and variable parameters in order to make them generic and
 reusable. When a module is instantiated, parameters can be replaced by
 constant- and state-level expressions, and these instantiations must be taken
 into account when generating proof obligations for back-end provers.

- Handling temporal logic. Proofs of liveness properties need support for
 reasoning about first-order temporal logic, such as induction over
 well-founded orderings. Fairness hypotheses require reasoning over the
 enabledness of actions. New backend provers need to be set up and integrated
 into TLAPS for carrying out these proofs.

- Improved backend provers. The current backend provers provide decent support
 for proof obligations mixing first-order logic, elementary set theory,
 functions, and integer arithmetic. Reasoning about other important data
 structures such as finite sequences requires low-level user interaction. We
 are interested in exploiting advances in automatic deduction techniques, such
 as support for relevant theories in SMT solvers, for enabling a higher degree
 of automation of such proof steps.

- Rigorous validation of soundness. Computing proof obligations involves some
 subtle transformations, such as distributing the prime operator of TLA+ or
 handling instantiated ENABLED expressions. We are working on a precise
 definition of the semantics of the proof language that would help us ensure
 the soundness of these transformations and give guidelines to the
 implementation.

- Checking SMT proofs. The SMT backend handles most of the proof obligations
 that occur in practice. The current version of TLAPS assumes the external SMT
 solver to be correct, but we are interested in reconstructing proofs provided
 by SMT solvers within Isabelle/TLA+. The Zenon backend already benefits from
 proof reconstruction.

- Performance issues. Proof projects can be large, and TLAPS implements
 mechanisms, such as fingerprinting proof obligations, that are intended to
 make the tool scale. Performance bottlenecks should be monitored and avoided,
 whenever possible.

- Case studies and proof libraries. Our work on TLAPS is validated by carrying
 out case studies, and we provide libraries of lemmas that are useful for many
 proof projects.

We do not expect to be able to address all of these issues within 24 months. The
choice of items will be made jointly with the research engineer, also depending
on his or her interests and background.


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

You should hold a PhD degree in computer science and have solid knowledge of
mathematical logic, as well as implementation skills related to symbolic theorem
proving. TLAPS is mainly implemented in OCaml, but some Java programming will be
necessary for interfacing TLAPS with the other TLA+ tools. Experience with
temporal and modal logics, with interactive theorem provers or with Eclipse
could be valuable.

Work on TLAPS provides the opportunity to learn about issues of using deductive
verification in practice, and there are possibilities to produce publishable
research. However, the main focus is 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.

Details
=======

Location

The research engineer can choose between working at the Microsoft Research -
Inria Joint Centre in Paris or at the LORIA laboratory in Nancy.

Compensation

The salary will be between 2900 and 3800 euros, depending on qualifications
and experience.

Duration

The post is for a duration of 2 years, extensible to a 3rd year (depending
on funding).

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
March 12, 2018. Please at least let us know by this date if you are interested
in the position or if you have any further questions.

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