Projet ANR-14-CE25-0005 – ELICA : Élargir les idées logiques pour l'analyse de complexité
Programme : Fondements du numérique (DS0705) 2014
Année de financement : 2014
Coordinateur du projet : Monsieur Damiano Mazza (Laboratoire d'Informatique de Paris Nord)
Partenaires : Institut national de recherche en informatique et en automatique; Laboratoire public; Laboratoire d'Informatique du Parallélisme
Montant : 398528.0 euros
Date de début : 2014
Durée : 60 mois
Résumé : 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.