Certification de la transformation de tâches de preuve
par Quentin Garchery
Mardi 25 janvier 2022 à 14h00
Salle 435 (salle des thèses), bâtiment 650 Ada Lovelace et en ligne
Résumé: De nombreux prouveurs et outils de vérification font un usage instensif des transformations logiques afin de ramener un problème exprimé sous la forme d'une tâche de preuve à un certain nombre de tâches de preuve plus simples à valider. Les transformations font souvent partie de la base de confiance de l'outil de vérification. Cette thèse a pour objectif de renforcer la confiance accordée aux transformations logiques. Les transformations sont instrumentées pour produire des certificats puis ceux-ci sont vérifiés par un outil externe: c'est l'approche sceptique. De ce fait, notre méthode est incrémentale et robuste aux modifications apportées au code des transformations. Nous définissons deux formats de certificats; les transformations génèrent des certificats de surface et ces certificats sont traduits en des certificats de noyau qui sont destinés à la vérification finale. L'accent est mis sur la facilité de production des certificats de surface et nous avons fait en sorte qu'ils soient, autant que possible, indépendants des tâches de preuve, facilitant ainsi leur composition et rendant la certification plus modulaire. Les certificats de noyau, au contraire, incluent de nombreux détails tout en restant élémentaires, de sorte que leur vérification est réalisable par un outil simple, dont la confiance est facile à établir. Nous proposons une procédure de traduction d'un certificat de surface en un certificat de noyau qui n'a pas besoin d'être certifiée. Les transformations logiques sont considérées dans une logique d'ordre supérieur avec polymorphisme de type, ce formalisme pouvant être étendu avec des théories interprétées telles que l'égalité ou l'arithmétique entière. Nous appliquons notre méthode à Why3, et notamment à des transformations complexes qui pré-existent à notre travail. Nous implémentons également deux vérificateurs de certificats, le premier reposant sur une approche calculatoire efficace et l'autre s'appuyant sur un encodage superficiel des tâches de preuve dans le framework logique Lambdapi, donnant ainsi de fortes garanties de sa correction.
Jury:
- Sandrine Blazy, Université de Rennes 1, Rapporteure
- Sylvain Boulmé, INP Grenoble 1, Rapporteur
- Stephan Merz, Inria Nancy, Examinateur
- Jorge Sousa Pinto, Université de Minho, Examinateur
- Mihaela Sighireanu, ENS Paris-Saclay, Examinatrice
- Claude Marché, Université Paris-Saclay, Directeur de thèse
- Chantal Keller, Université Paris-Salcay, Co-encadrante
- Andrei Paskevich, Université Paris-Saclay, Co-encadrant