2020-02868 - Ingénieur de recherche : vérification de systèmes paramétrés

Contract type : Fixed-term contract

Level of qualifications required : PhD or equivalent

Fonction : Temporary scientific engineer

Level of experience : Up to 3 years

Context

The VeriDis project team (https://team.inria.fr/veridis/) is a partner of the PARDI project (http://pardi.enseeiht.fr), funded by the French research agency, that also involves scientists in Toulouse and in the Paris area. The objective of the project is to contribute formal verification techniques for parameterized distributed systems: parameters can be the number of nodes, the kinds of possible failures or the communication mechanism. VeriDis has a strong background in formal proofs of parallel and distributed algorithms specified in the TLA+ formalism, and it contributes to the development of the interactive proof assistant TLAPS (http://tla.msr-inria.inria.fr/tlaps/content/Home.html) for TLA+, as well as to the symbolic model checker Apalache (https://forsyte.at/research/apalache/). The Toccata team of the research center Inria Saclay Ile de France, a partner in the PARDI project, develops Cubicle (http://cubicle.lri.fr), a tool for the automatic verification of parameterized systems. One of the objectives of PARDI is to establish a link between TLAPS and automatic verification tools such as Apalache or Cubicle in order to augment the degree of automation in the proof of TLA+ specifications.

Assignment

The engineer will be hired by Inria for the VeriDis project team and will work together with members of the Toccata team in order to link the techniques used in Apalache, Cubicle, and TLAPS. A fragment of TLA+ will be defined, together with translations into the input formats accepted by Apalache and Cubicle. A software architecture will be designed and implemented for calling these tools from within a proof carried out in TLAPS. As for Cubicle, besides its use as a black box, it will be of interest to make it compute explicit invariants of algorithms that can be injected into an interactive proof. It may be necessary to extend the algorithms for invariant computation that exist within Cubicle in order to adapt them for specific abstractions, such as the verification of fault-tolerant distributed algorithms.

The engineer will mainly work with Stephan Merz, as well as with Igor Konnov (VeriDis), Sylvain Conchon (Toccata), and Fatiha Zaïdi (Toccata).

Main activities

  • Get acquainted with TLA+ and the capabilities of the verification tools mentioned above.
  • Design a fragment of TLA+ than can be translated into Apalache and Cubicle.
  • Implement translators from the TLA+ into the input languages of the automatic tools.
  • Link TLAPS with Apalache and Cubicle based on the translators.
  • Study the computation of invariants of distributed algorithms specified in TLA+.
  • Document the above techniques and the code.
  • Interact with the partners of the PARDI project.

Skills

Technical skills and level required : thesis in computer science, formal methods

Languages : English or French

Relational skills : suggest original techniques, be able to discuss with partners on-site and remotely

 

Benefits package

  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
  • Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage

Remuneration

Remuneration according to diploma and experience from 2632€ gross