Stage: Traitement des grands opérateurs dans l’outil Why3

Le centre de recherche Inria de Saclay a été créé en 2008. Sa dynamique s’inscrit dans le développement du plateau de Saclay, en partenariat étroit d’une part avec le pôle de l’Université Paris-Saclay et d’autre part avec le pôle de l’Institut Polytechnique de Paris . Afin de construire une politique de site ambitieuse, le centre Inria de Saclay a signé en 2021 des accords stratégiques avec ces deux partenaires territoriaux privilégiés.

Le centre compte 40 équipes-projets , dont 32 sont communes avec l’Université Paris-Saclay ou l’Institut Polytechnique de Paris. Son action mobilise plus de 600 personnes, scientifiques et personnels d’appui à la recherche et à l’innovation, issues de 54 nationalités.

Le centre Inria Saclay - Île-de-France est un acteur essentiel de la recherche en sciences du numérique sur le plateau de Saclay. Il porte les valeurs et les projets qui font l’originalité d’Inria dans le paysage de la recherche : l’excellence scientifique, le transfert technologique, les partenariats pluridisciplinaires avec des établissements aux compétences complémentaires aux nôtres, afin de maximiser l’impact scientifique, économique et sociétal d’Inria.

Le logiciel Why3 [1], développé dans l’équipe Toccata de l’Inria Saclay, est un outil de
vérification déductive. Il propose un langage logique, un langage de programmation et une
interface avec des démonstrateurs automatiques et interactifs. Ce stage a pour but d’améliorer le support par l’outil Why3 de théories logiques définissant de grands opérateurs.

[1] L’outil Why3. https://www.why3.org/

Ce stage a pour but d’améliorer le support par l’outil Why3 de théories logiques définissant
de grands opérateurs tels que

  sum_{x∈s} f (x)

pour un ensemble fini s. De telles théories existent deja dans la bibliotheque standard de Why3,
dans le cas particulier ou s est un intervalle d’entiers [2]. Un premier objectif est d’en generaliser
la definition a des ensembles finis quelconques et pour d’autres operateurs que la somme (produit, cardinal, maximum, etc.). On pourra notamment s’inspirer de ce qui est fait dans la bibliotheque Coq Mathematical Components [3], et notamment ses bibliotheques finfun et bigop.
Un second objectif est d’ameliorer le support de telles theories par les demonstrateurs automatiques de type SMT interfaces avec Why3 (Alt-Ergo, CVC5, Z3, etc.). On pourra en particulier exploiter la theorie des ensembles finis qui existe dans certains demonstrateurs comme CVC5 [5], et s’inspirer d’un article de Leino et Monahan sur le support des grands operateurs
dans Spec# [4].

[2] Bibliotheque Int de Why3. https://www.why3.org/stdlib/int.html
[3] Mathematical Components. https://math-comp.github.io/
[4] Rustan Leino, Rosemary Monahan. Automatic Verification of Textbook Programs that Use
Comprehensions. In FTfJP ’07 : Proceedings of the 9th Workshop on Formal Techniques for
Java-like Programs, 2007.
[5] Theorie “Finite Sets” du demonstrateur SMT CVC5. https://cvc5.github.io/docs/
cvc5-1.1.2/theories/sets-and-relations.html

• Restauration subventionnée
• Transports publics remboursés partiellement
• Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
• Possibilité de télétravail (après 6 mois d'ancienneté) et aménagement du temps de travail
• Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
• Accès à la formation professionnelle
• Sécurité sociale