Détails sur le séminaire

Résumé : Bonjour à tous,
J'ai le plaisir de vous inviter à ma soutenance de thèse, intitulée
« Automated verification of termination certificates »
Vous êtes chaleureusement invités au pot qui suivra et qui se déroulera au même endroit.
Jury :
Mr Frédéric Blanqui, Chargé de recherche à l’INRIA, Paris, Co-Directeur de thèse
Mr David Delahaye, Maître de conférence au CNAM, Paris, Examinateur
Mme Catherine Dubois, Professeure à l’ENSIIE, Évry, Rapporteur
Mme Dominique Duval, Professeure à l’Université Joseph Fourier, Grenoble, Examinatrice
Mr Jean-François Monin, Professeur à l’Université Joseph Fourier, Grenoble, Directeur de thèse
Mr René Thiemann, Priv.-Doz. Dr. University of Innsbruck, Austria, Rapporteur
Résumé :
S'assurer qu'un programme informatique se comporte bien, surtout dans des applications critiques (santé, transport, énergie, communications, etc.) est de plus en plus important car les ordinateurs et programmes informatiques sont de plus en plus omniprésents, voir essentiel au bon fonctionnement de la société. Mais comment vérifier qu'un programme se comporte comme prévu, quand les informations qu'il prend en entrée sont de très grande taille, voire de taille non bornée a priori ? Pour exprimer avec exactitude ce qu'est le comportement d'un programme, il est d'abord nécessaire d'utiliser un langage logique formel. Cependant, comme l'a montré Gödel dans, dans tout système formel suffisament riche pour faire de l'arithmétique, il y a des formules valides qui ne peuvent pas être prouvées. Donc il n'y a pas de programme qui puisse décider si toute propriété est vrai ou fausse. Cependant, il est possible d'écrire un programme qui puisse vérifier la correction d'une preuve. Ce travail utilisera justement un tel programme, Coq, pour formellement vérifier la correction d'un certain programme. Dans cette thèse, nous expliquons le développement d'une nouvelle version de Rainbow, plus rapide et plus sûre, basée sur le mécanisme d'extraction de Coq.
La version précédente de Rainbow vérifiait un certificat de terminaison en deux étapes. Premièrement, elle utilisait un programme OCaml non certifié pour traduire un fichier CPF en un script Coq, en utilisant la bibliothèque Coq sur la théorie de la réécriture et la terminaison appelée CoLoR. Deuxièmement, elle appelait Coq pour vérifier la correction du script ainsi généré. Cette approche est intéressante car elle fournit un moyen de réutiliser dans Coq des preuves de terminaison générée par des outils extérieurs à Coq. C'est également l'approche suivie par CiME3. Mais cette approche a aussi plusieurs désavantages. Premièrement, comme dans Coq les fonctions sont interprétées, les calculs sont beaucoup plus lents qu'avec un langage où les programmes sont compilés vers du code binaire exécutable. Deuxièmement, la traduction de CPF dans Coq peut être erronée et conduire au rejet de certicats valides ou à l'acceptation de certificats invalides. Pour résoudre ce deuxième problème, il est nécessaire de dénir et prouver formellement la correction de la fonction vérifiant si un certicat est valide ou non. Et pour résoudre le premier problème, il est nécessaire de compiler cette fonction vers du code binaire exécutable.
Cette thèse montre comment résoudre ces deux problèmes en utilisant l'assistant à la preuve Coq et son mécanisme d'extraction vers le langage de programmation OCaml. En effet, les structures de données et fonctions définies dans Coq peuvent être traduites dans OCaml et compilées en code binaire exécutable par le compilateur OCaml. Une approche similaire est suivie par CeTA en utilisant l'assistant à la preuve Isabelle et le langage Haskell.