L'Agence nationale de la recherche Des projets pour la science

Translate this page in english

Fondements du numérique (DS0705) 2014
Projet ELICA

Élargir les idées logiques pour l'analyse de complexité

L'analyse statique de complexité vise à donner des méthodes pour déterminer la quantité de ressources (temps de calcul,
mémoire) nécessaires à l'exécution d'un programme. Il est bien connu que ce problème est indécidable en général. Néanmoins, il est possible d'envisager des méthodes (correctes) qui couvrent un grand nombre de cas, et si possible ceux que l'on rencontre en pratique.
Le but du projet ELICA est de développer les méthodes logiques pour l'analyse statique de complexité de programmes, d'en améliorer l'expressivité et d'élargir leur portée pour les appliquer à des paradigmes de calculs non-déterministes et concurrents.
Les outils d'origine logique, en particulier issus de la théorie de la démonstration, ont démontré être d'importance capitale pour l'analyse statique de complexité. Des critères garantissant des bornes de complexité ont été formulés (notamment par les participants au projet ELICA) à l'aide de restrictions structurelles sur le lambda-calcul, de sous-systèmes de la logique linéaire où l'élimination des coupures a une complexité limitée, de systèmes de types pour les langages fonctionnels, et de méthodes sémantiques (interprétations polynomiales et sémantique dénotationnelle). Ces méthodes ne donnent pas des bornes fines sur la complexité du programme, mais elles ont l'avantage d'être modulaires et de produire des certificats facilement vérifiables.
Toutefois, à présent ces méthodes ne s'appliquent qu'à un spectre relativement restreint de langages, tous de nature plus ou moins fonctionnelle. Même dans le cas fonctionnel, les critères restent peu satisfaisants au niveau de l'expressivité, c'est-à-dire, du nombre de programmes pratiques auxquels ils peuvent être appliqués. Le projet ELICA se pose comme objectif de développer les méthodes logiques existantes et d'en introduire des nouvelles, afin:
- d'améliorer l'expressivité des critères d'analyse statique dans le cas fonctionnel du premier ordre, mais surtout d'élargir la portée de ces critères à la complexité d'ordre supérieur (en particulier, d'ordre 2, ou type-2), qui reste encore relativement peu explorée ;
- d'augmenter l'impact pratique de ces méthodes en définissant des critères de complexité pour des languages avec caractéristiques impératives, et en les reliant aux critères pour la vérification de propriétés de sécurité (non-interférence) ;
- d'appliquer ces méthodes à des contextes non-déterministes et probabilistes, pour analyser la complexité de programmes implémentant des algorithmes aléatoires, avec le but à long terme d'utiliser ces méthodes pour l'analyse de protocoles cryptographiques et de sécurité ;
- d'élargir la portée de ces méthodes à l'analyse de systèmes concurrents. Ici, le problème est de nature avant tout fondationnelle, car à présent il n'existe pas de définition générale de complexité pour les processus concurrents. Nous proposons donc de développer d'abord une théorie de la complexité des comportements interactifs (généralisant les fonctions), capable de donner un contenu formel à des notions comme le temps de réponse à une requête, l'espace mémoire utilisé, le nombre de processus, etc. Ensuite, nous étudieront l'application de méthodes logiques à cette théorie.

Partenaires

Inria Institut de Recherche en Informatique et en Automatique

LIPN Laboratoire d'Informatique de Paris Nord

LIP Laboratoire de l'Informatique du Parallélisme

Aide de l'ANR 398 528 euros
Début et durée du projet scientifique octobre 2014 - 48 mois

 

Programme ANR : Fondements du numérique (DS0705) 2014

Référence projet : ANR-14-CE25-0005

Coordinateur du projet :
Monsieur Damiano Mazza (Laboratoire d'Informatique de Paris Nord)

 

Revenir à la page précédente

 

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.