Contract type : Public service fixed-term contract
Level of qualifications required : Graduate degree or equivalent
Fonction : PhD Position
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 and involves collaboration with experts in synchronous languages (Marc Pouzet), verified compilation (Xavier Leroy) and automatic verification (Cesare Tinelli).
Initial work on the Vélus compiler treated the basic features of Lustre: simple equations, initialized delays, and function instantiations. Recent PhD work has extended the semantic model and compilation passes with the modular reset construct from the Scade language. This PhD would focus on progressively adding state machines. Please see the Vélus website for other scientific references.
The first challenge is to adapt existing state machine semantic models for use within an interactive theorem prover. The definitions must be consistent with intuitions about the construct, suitable for verifying compilation passes, and amenable to program verification. State machines are compiled by rewriting them into a smaller subset of the language. The second challenge is to implement the rewrite rules as a functional program in Coq and to prove that it preserves the semantics of source programs.
The PhD student will work closely with other team members to develop semantic models, compilation passes, and correctness proofs for the state machine construct. Results will be communicated to international workshops, conferences, and journals.
Over the three years of the PhD scholarship, a hard-working candidate would master advanced concepts in programming languages and their semantics, become an expert in interactive theorem proving and its application to compiler development, and contribute to extending the state-of-the-art in formal techniques for model-based development. Students join a passionate research group. They learn how to analyze and solve challenging technical problems, present results at workshops and conferences, write scientific articles, and collaborate with other researchers. At the end of a successful PhD, the candidate will be well prepared to continue a research career or contribute to cutting edge developments in industry.
- Master relevant background knowledge on synchronous language semantics and compilation, and interactive theorem proving by reading books and research articles.
- Develop a plan of action based on successively treating the various state machine features described in the literature.
- Extend the existing Vélus compiler with required constructs and define semantic models for them in the Coq ITP.
- Implement compilation algorithms in Coq and develop proofs of semantic preservation.
- Document the results in scientific articles and a PhD thesis.
- Participate in workshops and team activities.
- (Optional) Contribute to teaching by supervising lab and tutorial sessions.
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 : 3 years
- Deadline to apply : 2019-10-31
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.
Ideally, you have had some exposure to interactive theorem proving in your undergraduate or masters programs—just to be sure that the subject suits you.
A curiosity to master new topics, an openness to criticism, a willingness to learn and improve, and a critical mind are essential.
Knowledge of Lustre, Scade, or Model-Based Development is optional.
Any PhD involves focusing on a narrow topic for three (long!) years. Additionally, developing large projects in interactive theorem provers requires a particular kind of tenacity and stamina.
It would be possible to undertake a five month (M2) internship in the team before beginning the PhD (or deciding not to).
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.