Contract type : Fixed-term contract
Level of qualifications required : PhD or equivalent
Fonction : Temporary scientific engineer
Level of experience : Up to 3 years
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.
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).
- 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.
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
- 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 according to diploma and experience from 2632€ gross
- Theme/Domain :
Proofs and Verification
Software engineering (BAP E)
- Town/city : Villers lès Nancy
- Inria Center : CRI Nancy - Grand Est
- Starting date : 2020-09-01
- Duration of contract : 1 year, 4 months
- Deadline to apply : 2020-08-17
The keys to success
The candidate has a doctorate in computer science and strong experience in formal methods for the verification of systems or algorithms (model checking, SMT solving, possibly automated or interactive theorem proving). He or she has experience in the design and implementation of software tools, preferably in OCaml or similar functional languages. Prior knowledge of TLA+ is not required.
The candidate knows how to work in a group, including remotely with off-site partners. He or she will be able to design algorithms and present, implement, and document them rigorously.
Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.