Damien Pous, ERC Starting Grant 2015

Vérification et certification sont deux approches complémentaires pour s’assurer du bon fonctionnement des programmes et machines. La vérification permet de voir si un programme satisfait une propriété (pas de division par 0 par exemple). La vérification se réalise généralement avec des outils automatiques, mais ces outils sont souvent confrontés à une explosion combinatoire : ils ne peuvent pas toujours être utilisés car ils nécessitent trop de temps de calcul. 
La certification quant à elle garantit les programmes à un niveau très fort. Pour cela, il est nécessaire de rédiger une preuve mathématique, c’est-à-dire décrire et justifier dans les moindres détails tout ce que le programme est censé faire ou non. Afin de s’assurer de la correction de cette preuve, on utilise aujourd’hui l’ordinateur, via des assistants de preuve comme Coq ou Isabelle / HOL. Mais cette étape est très lourde, et demande du temps et de l’expertise, même pour des tâches de base qui pourraient être obtenues facilement par vérification. On cherche donc à automatiser au maximum la rédaction de ces preuves, en intégrant divers algorithmes dans ces assistants de preuve. 

Pour avancer dans cette direction, Damien Pous se base sur une nouvelle approche issue du domaine de la théorie de la concurrence, champ de recherche dans lequel il a réalisé sa thèse. Dans un travail récent avec Filippo Bonchi, il a en effet obtenu un algorithme pour une brique de base en vérification, qui est plus rapide d’un ordre de grandeur que ceux utilisés dans les outils actuels. En effet, grâce à leur expertise, les chercheurs ont pu détecter et améliorer une utilisation implicite de la coinduction, outil bien connu de la théorie de la concurrence, dans un algorithme dû à Hopcroft et Karp et communément utilisé en vérification. En exploitant pleinement ce levier, ils comptent rendre ces outils de vérification beaucoup plus efficaces, et donc plus largement utilisables, notamment dans l’industrie. 

Plus précisément dans ce cas, pour vérifier qu’un programme satisfait une propriété, une approche est de transformer le programme et la propriété en automates, qui sont des objets mathématiques finis, dont on peut avoir une vision complète. Intuitivement, nous pourrions dire que les deux seraient des damiers où, pour le programme, le blanc représenterait ce qui est possible et le noir impossible, et pour la propriété, le blanc serait ce qui est autorisé et le noir interdit. En comparant ces deux objets à l’aide d’algorithmes d’automates, il est ainsi possible de vérifier que le blanc du programme est inclus dans le blanc de la propriété : le programme reste toujours dans la zone autorisée. L’algorithme sus-cité n’a été étudié que pour la forme la plus simple d’automates. La question se pose donc de l’étendre à des classes d’automates plus complexes, permettant la vérification de programmes plus compliqués, vis à vis de propriétés plus expressives. Un autre domaine où Damien Pous utilise la coinduction est le calcul des relations. Il y est également question de comparaison, mais cette fois-ci entre des ensembles de graphes, qui représentent ces relations. On cherche alors non seulement à comparer automatiquement ces ensembles, mais aussi à axiomatiser, c’est-à-dire définir le socle de lois régissant les opérations sur les relations. Le rapprochement du domaine des automates et du calcul des relations est une approche originale dans ce projet. 

En s’appuyant sur ces travaux sur la vérification et le calcul de relations, le but de l’ERC de Damien Pous est double. Tout d’abord, il s’agit de fournir des techniques d’automatisation puissantes au sein d’outils de certification tels que Coq, pour que les parties rébarbatives soient confiées à l’ordinateur, qui obtiendrait certaines preuves par lui-même, par calcul. L’assistant de preuve qui était alors comme un professeur de mathématiques sévère serait ainsi secondé par une personne pour l’aide aux devoirs. 
D’autre part, l’implémentation des algorithmes développés simplifierait les calculs, qui gagneraient alors de façon très significative en efficacité, permettant de fournir des outils de vérification efficients et certifiés allant au-delà de ce qui existe actuellement.