2019-02247 - Doctorant F/H Doctorant / Preuves et vérification

Type de contrat : CDD

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : Doctorant

Contexte et atouts du poste

SMTCoq [AFG+11, EMT+17, HR19] is a plugin for the Coq interactive theorem prover, devel-oped in collaboration between Université Paris-Saclay, the University of Iowa (US), the Univer-sity of Stanford (US) and Inria Sophia Antipolis Méditerranée.Its goal is to make Coq interact with external, automatic theorem provers based on satisfia-bility (SAT and SMT), with a twofold objective :

  • increase confidence in automatic provers, which are large programs that may be buggy, bychecking the answers they give;
  • increase Coq automation by offering the possibility to call automatic provers withoutcompromising soundness.

SMTCoq thus allows users to automatically prove Coq goals mixing arithmetic reasoning anddata structures such as vectors, arrays, . . . by integrating various competitive automatic solverssuch as CVC4 and veriT.The heart of SMTCoq is a checker forproof certificatescoming from automatic provers,implemented and proved correct inside Coq. This checker is able to check in a very efficientand modular way answers coming from different SAT and SMT solvers. On top of this checker,new Coq tactics allow users to call automatic solvers on Coq goals, automatically checking theanswers.The objective of the internship is to reinforce the expressivity of these tactics in such a waythat Coq users can enjoy as much automation as possible.

Mission confiée

In order to get familiar with SMTCoq, the first month of internship will focus on one or multiplepractical aspects :

  • handle the various notions of equality in Coq, and allow the users to add new ones andlink them with the SMT notion of equality;
  • implement various algorithms to select the context to be sent to the automatic solvers, asproposed in the literature; . . .

The internship will then focus on aspects mixing theory and practice: (1) propose a newmethod to encode the expressive logic of Coq into the less expressive logics of automatic proversand (2) establish its correctness. The originality of this new encoding will be to be fine grained,meaning that it will consist in small, simple encodings, each of them tackling one aspect of Coq’s logic. It allows one to make a modular proof of correctness, and offers a better composabilityof encodings and the possibility to incrementally add new ones on demand. Depending on thenature of the encodings, their correctness proofs will be performed directly (as a Coq proof)or by outputting certificates that will be checkeda posteriori, following the SMTCoq generalapproach.

Principales activités

Handle the various notions of equality in Coq, and allow the users to add new ones andlink them with the SMT notion of equality;

Implement various algorithms to select the context to be sent to the automatic solvers, asproposed in the literature; . .

Avantages

  • 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

Rémunération

Monthly salary (1st and 2nd year) : 1.982 euros - (3rd year) : 2.085 euros