DS0705 - Fondements du numérique

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

Résumé de soumission

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.

Coordination du projet

Damiano Mazza (Laboratoire d'Informatique de Paris Nord)

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.

Partenaire

LIPN Laboratoire d'Informatique de Paris Nord
LIP Laboratoire de l'Informatique du Parallélisme
Inria Institut de Recherche en Informatique et en Automatique

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

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter