Combiner types gradés et intersections pour l'analyse de ressources – CoGITARe

Les systèmes de types permettent de vérifier des propriétés de sécurité sur de gros programmes. Ce projet entend étendre la méthodologie à un plus grand panel de propriétés actuellement inaccessible dans l'état de l'art; permettant, en particulier, l'analyse de propriétés quantitatives.

Nous développerons une méthode pour récupérer des information d'ordre extensionelles dans les types des programmes. De cette manière, il sera possible de faire toute l'analyse statique au niveau des types. Dans ce but, nous allons combiner deux systèmes de types (ré)émergent, à savoir les types gradés et les types intersections, avec des techniques extraites de l'interprétation abstraite telles que le widdenning.

Les types gradés consistent à ``grader'' les types par une information extensionelle extraite d'une structure du premier ordre; les types intersections permettent de contourner la non-compositionalité intrinsèque des analyses fines. Ces deux propriétés nous permettraient de dépasser les deux plus grandes barrière technologiques pour appliquer efficacement l'interprétation abstraite en programmation fonctionnelle.