Composition du jury :

La méthode B réduit la correction du développement logiciel à la vérification d’obligations de preuve ; ses garanties reposent donc sur les outils qui déchargent ces obligations et sur les traductions qui les y acheminent. Cette thèse étudie deux voies, automatique et interactive, pour décharger les obligations de preuve B et établit pour chacune ce que signifie une obligation déchargée.

BEer est un encodeur vérifié des obligations d’Atelier B vers SMT-LIB. Les objets de B étant des ensembles et les termes de SMT-LIB portant une sorte fixe, une valeur B admet plusieurs représentations cibles, un ensemble devenant un prédicat caractéristique, et une relation fonctionnelle une fonction. La relaxation de types ordonne ces représentations et fait passer les termes de l’une à l’autre sans en changer la sémantique. Le théorème de correction énonce que tout encodage réussi d’un terme bien typé et bien défini possède une sémantique compatible avec sa source à la représentation choisie ; en particulier, pour les obligations de preuve, la véracité est préservée.

BARReL, développé avec Ghilain Bergeron, importe la méthode B dans Lean. Il fait de la bonne définition des opérateurs partiels une contrainte de typage, si bien qu’aucun terme n’est construit sans preuve de sa bonne définition, décharge automatiquement les buts de routine et laisse les autres à la preuve interactive dans Lean.

Chaque développement précise ce qu’il prouve et ce qu’il suppose, afin qu’une automatisation toujours plus puissante, y compris assistée par l’IA, puisse servir sans que la validité d’un résultat dépende de l’outil qui l’a proposé.