2019-01951 - PhD Position F/M Semantics and Compilation of State Machines in an Interactive Theorem Prover

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

Context

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).

Assignment

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.

Main activities

  1. Master relevant background knowledge on synchronous language semantics and compilation, and interactive theorem proving by reading books and research articles.
  2. Develop a plan of action based on successively treating the various state machine features described in the literature.
  3. Extend the existing Vélus compiler with required constructs and define semantic models for them in the Coq ITP.
  4. Implement compilation algorithms in Coq and develop proofs of semantic preservation.
  5. Document the results in scientific articles and a PhD thesis.

Additional activities:

  1. Participate in workshops and team activities.
  2. (Optional) Contribute to teaching by supervising lab and tutorial sessions.

Skills

Languages: French or English.

 

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