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
Abstract: In various provers and deductive verification tools, logical transformations are used extensively in order to reduce a proof task into a number of simpler tasks. Logical transformations are often part of the trusted base of such tools. In this thesis, we develop a framework to improve confidence in their results. We follow a skeptical approach: transformations are instrumented to produce certificates that are checked by a third-party tool. Thus, we benefit from a modular approach that is also robust to changes in the source code of the transformations. We design two kinds of certificates. Transformations produce surface certificates that are then translated to kernel certificates which are destined for final verification. We made sure that surface certificates are easy to produce. Moreover, surface certificates are as independent of the transformation application as possible and this makes for a modular certification. On the contrary, kernel certificates include numerous details about the transformation application and are kept elementary. This helps to define simpler checkers and establish their correctness. We propose a translation procedure from surface certificates to kernel certificates which does not need to be trusted. Logical transformations are considered in a higher-order logic, with type polymorphism and built-in theories such as equality and integer arithmetic. We apply our framework to Why3 and use it to instrument pre-existing and complex transformations. Additionally, we implement two certificate checkers. The first one follows an efficient computational approach while the second is based on a shallow embedding of proof tasks inside the logical framework Lambdapi, thus exhibiting formal guaranties of its correctness.
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