Liens transverses ENS de Lyon

Projet ERC "CoVeCe" de Damien Pous

Domaine : Morphogenèse

Recherche : Co-induction pour la vérification et la certification (Coinduction for Verification and Certification)


Services et outils

L'ENS de Lyon conseille et accompagne les chercheurs dans leurs projets. Elle propose également des équipements de haute performance.

En savoir plus

Zoom sur

Description

Description du projet

Les bugs logiciels et matériels coûtent des centaines de millions d’euros chaque année aux entreprises et administrations. Vérification et certification sont cruciales afin de concevoir des programmes et des machines plus sûres. Mais ces méthodes se heurtent à des difficultés de mises en œuvre et d’efficacité. Grâce à une nouvelle approche issue de la théorie de la concurrence, Damien Pous, chercheur CNRS au sein du Laboratoire d’informatique du parallélisme (LIP - CNRS/ENS Lyon/Université de Lyon), souhaite dans son ERC CoVeCe proposer de nouveaux algorithmes pour révolutionner ces outils, et ainsi obtenir des machines et des programmes plus sûrs.

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. (©CNRS)

Financement ERC : 

1 407 413 €

Durée : 

1er avril 2016 au 31 mars 2021

ERC Starting Grant

Les subventions ERC Starting Grant sont destinées aux jeunes chercheurs possédant entre 2 à 7 ans d’expérience depuis l’obtention de leur doctorat. L'objectif des bourses Starting Grant est de permettre à des jeunes scientifiques de constituer leur équipe de recherche autour d'un thème original. Les recherches doivent être menées dans un institut de recherche public ou privé situé dans un État membre de l’UE ou un pays associé. La durée de la bourse est de 5 ans et les critères de sélection sont l'excellence scientifique du projet et du chercheur qui le porte. Ce dernier doit faire preuve de son indépendance scientifique et de sa capacité à assumer la gestion de son projet.

Chercheur

Damien PousDamien Pous

Directeur de recherche au LIP de l'ENS de Lyon

Page personnelle de Damien Pous

Type de page
Discipline(s)
Mots clés