Contract type : Fixed-term contract
Renewable contract : Oui
Level of qualifications required : PhD or equivalent
Fonction : Post-Doctoral Research Visit
Level of experience : Up to 3 years
The FidelR project, for “Fidelity in Reactive Systems Design and Compilation”, is funded by a French government “Young Researcher” grant (ANR JCJC). Its goal is to extend the Vélus verified Lustre compiler with state machines and techniques for interactively verifying models. The grant includes funding for national and international travel to participate in workshops and conferences.
Lustre is a synchronous language closely related to the industrial Scade tool which supports Model-Based Development (MBD) of critical embedded control software. It's a programming language with a formal semantics for block-diagram specifications.
The Vélus compiler is developed in OCaml and the Coq Interactive Theorem Prover (ITP). It successively transforms source programs into the Clight language used by CompCert. The overall correctness theorem states that the stream-based semantics of the source program is preserved by the generated assembly code.
Vélus is developed in the Inria PARKAS team located at the École normale supérieure in the heart of Paris. Development is led by [Timothy Bourke](https://www.tbrk.org) and involves collaboration with experts in synchronous languages (Marc Pouzet), verified compilation (Xavier Leroy) and automatic verification (Cesare Tinelli).
Work on Vélus has to date focused on verified compilation. This postdoctoral position would involve developing techniques and tools for interactively verifying Lustre programs within Coq. That is, making it possible to load a Lustre program into Coq, to state invariants, and to prove that the program satisfies them. The compiler correctness theorem guarantees that such invariants also hold of the generated code. While interactive frameworks exist for imperative languages, like the Verified Software Toolchain and Isabelle/SIMPL, and model checkers exist for synchronous languages, like Kind 2 and Lesar, there are relatively few results on the interactive verification of languages for model-based development. We believe that ITPs provide an ideal environment for decomposing verification goals, safely mixing results from model-checkers and specialized tactics, and transferring properties of the model to generated executables.
The postdoctoral researcher will collaborate closely with other team members to develop techniques and tools for interactively verifying Lustre programs in the context of the Vélus project. Please see the Vélus website for scientific references. This work will involve mastering the existing semantic models, proposing verification techniques, implementing plugins and tactics in the Coq ITP, and working on case-studies to guide and evaluate the approach. Results will be communicated to international workshops, conferences, and journals.
The initial contract is for one year, but solid progress on research goals would open other opportunities.
- Master relevant background knowledge on synchronous languages and the state-of-the-art in interactive program verification by reading books and research articles.
- Experiment with small examples in the Coq ITP to understand the problem and potential solutions.
- Propose verification techniques and implement them as Coq plugins and tactics.
- Evaluate the techniques and implementations on one or more larger case studies.
- Document the results in technical reports and scientific articles.
- Participate in workshops and team activities.
- (Optional) Teach at the L3 and masters level.
Technical skills and level required:
- Strong expertise in one or more programming languages (ideally a strongly typed functional language like OCaml, SML, or Haskell).
- Some experience with Interactive Theorem Proving or a very strong motivation to become a specialist.
Languages: French or English.
- 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
- Theme/Domain :
Proofs and Verification
Software engineering (BAP E)
- Town/city : Paris
- Inria Center : CRI de Paris
- Starting date : 2020-01-01
- Duration of contract : 1 year
- Deadline to apply : 2019-11-30
The keys to success
You are passionate (but not fanatical!) about functional languages and interactive proof assistants. You are not (just) interested in the theory of logic, but really motivated to apply it to real-world problems. Tenacity and a taste for simplicity are essential character traits for this work.
You have completed, or will soon complete, a PhD in computer science, computer engineering, or mathematics with a strong emphasis on formal methods, verification, programming language semantics, or computer-assisted logic. You already have some experience with interactive theorem proving, but may not (yet!) be an expert. Ideally, you have already contributed to software projects or publications.
Knowledge of Lustre, Scade, or Model-Based Development is not essential.
Inria, the French national research institute for the digital sciences, promotes scientific excellence and technology transfer to maximise its impact. It employs 2,400 people. Its 200 agile project teams, generally with academic partners, involve more than 3,000 scientists in meeting the challenges of computer science and mathematics, often at the interface of other disciplines. Inria works with many companies and has assisted in the creation of over 160 startups. It strives to meet the challenges of the digital transformation of science, society and the economy.
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.