Prix de thèse Gilles Kahn et Prix La Recherche pour Amina Doumane
Quand on interroge Amina Doumane sur son domaine de recherche, on réalise vite que l’on va devoir la suivre dans une certaine gymnastique intellectuelle, façon mise en abyme à la Inception. Le but de sa thèse était de prouver qu’une preuve est bien une preuve. Mais évidemment pas n’importe quelle preuve…
Cette post-doctorante au Laboratoire d’informatique du parallélisme (LIP - CNRS/ENS Lyon/Université de Lyon), qui a mené sa thèse entre l’Institut de Recherche en Informatique Fondamentale (IRIF - CNRS/Université Paris-Diderot) et le Laboratoire Spécification et Vérification(LSV - CNRS/ENS Paris-Saclay) vient d’obtenir à la fois le prix de thèse Gilles Kahn décerné par la SIF, et le Prix La Recherche, pour le domaine sciences de l’information, pour son article présenté au LICS2017.
Dans les preuves mathématiques « normales », celles que l’on a pu faire au lycée, on nous a appris à s’appuyer sur des axiomes, c’est-à-dire des énoncés qui sont trivialement vrais, pour les utiliser pour démontrer des choses de plus en plus complexes. « Dans une démonstration infinitaire, aussi appelée preuve circulaire, lorsqu’on me donne un théorème T à démontrer, je peux utiliser T comme axiome pour démontrer … T ! précise la chercheuse. Les preuves circulaires sont très utiles, puisqu’elles facilitent la recherche de preuve, mais on n’avait pas jusque-là pu prouver qu’elles « méritaient » le nom de preuve », en d’autre termes qu’elles avaient les propriétés structurelles pour être désignées comme telles ».
Ces preuves circulaires, un peu inhabituelles vont s’avérer utiles pour la vérification de systèmes. Un système réactif correspond à peu près à n’importe quoi qui interagit avec son environnement, et qui évolue dans le temps : un ascenseur, une machine à café, une centrale nucléaire… La vérification d’un système correspond au fait de s’assurer que le système satisfait certaines propriétés, répond aux attentes qu’on peut en avoir, appelées spécifications : si j’appuie sur le bouton de la machine à café, j’obtiens un café… Pour pouvoir utiliser ces notions, on va alors abstraire, remplacer le système et les spécifications par des objets de logique que l’on sait manipuler. En l’occurrence, Amina Doumane s’est intéressée au µ-calcul, une forme de logique spécifique pour la description du comportement de système, notamment avec la prise en compte de la notion de temps.
Une première formule du µ-calcul va ainsi décrire le système, et une deuxième formule détaillera les propriétés attendues de ce système. Une 3e formule doit englober les deux premières, pour que la formule du système implique nécessairement la formule de la spécification. « Appelons cette formule « la grande implication », précise-t-elle. Si on ne parvient pas à prouver la grande implication, c’est que le système ne vérifie pas les spécifications. Mais si on la prouve, on est sûr que le système satisfait la spécification. De plus, cette preuve peut être vue comme un certificat, qui peut être communiqué et même exécuté. Cette technique est d’ailleurs plus informative que d’autres : la preuve nous apprend pourquoi le système vérifie la propriété, ce qui donne des éléments explicatifs et donc une confiance supplémentaire. »
Le tour de force d’Amina Doumane a été de réussir à concevoir un algorithme capable de prendre une formule de µ-calcul (par exemple et en particulier la grande implication) et d’en construire automatiquement une preuve. Comme souvent dans le cas d’avancées remarquables en recherche, l’ingéniosité a été de concilier des outils de disciplines différentes. Amina Doumane a ainsi pioché dans les algorithmes qu’utilise la théorie des automates, qu’elle a interprétés comme des algorithmes de recherche de preuve, dans les systèmes de preuves circulaires.
Par ses travaux dans sa thèse, elle a ainsi pu démontrer que les preuves circulaires se comportent réellement comme des preuves, et de façon secondaire fournir des algorithmes de traitement de µ-calcul en vue d’applications pour la vérification des systèmes.
Publications :
Thèse : « Théorie de la démonstration infinitaire pour les logiques à points fixes »
Article présenté à LICS17 : « Constructive completeness for the linear-time μ-calculus »
Publication commune avec Binaire, le blog informatique du Monde