Thursday 2 July 2020, 10:00, online: Certification modulaire de Why3, Quentin Garchery (PhD student, VALS, LRI, Univ. Paris-Saclay).

Cet exposé a pour objectif de présenter une approche modulaire de la vérification formelle en ayant pour application la certification de l'outil de vérification déductive Why3. Why3 est un outil de vérification de programmes (correction fonctionnelle, absence d'erreur à l'exécution, ...). Pour vérifier un programme, Why3 génère une formule appelée tâche de preuve qui devra être validée pour s'assurer que le programme est correct. Pour ce faire, il est possible de modifier la tâche de preuve en appliquant des transformations logiques et, en bout de chaîne, Why3 permet d'appeler différents prouveurs automatiques (CVC4, Z3, ....) afin de clore la vérification.

Le travail présenté vise à améliorer la confiance que l'on peut porter à Why3 en se concentrant sur les transformations logiques. Je présenterai la méthode mise en place pour permettre de les vérifier : il s'agit d'abord de définir un cadre permettant de les instrumenter à l'aide de certificats, ceux-ci étant alors vérifiés dans un deuxième temps. Les vérificateurs de certificats pouvant être définis de manière indépendante, je détaillerai deux implémentations, l'une en OCaml et l'autre se basant sur Dedukti. Ensuite je présenterai une amélioration de la méthode afin de faciliter l'ajout de certificats à une transformation et je donnerai des exemples d'applications, notamment à des transformations préexistantes.