Description
Date depot: 17 février 2023
Titre: Analyse statique par interprétation abstraite des langages fonctionnels et application à l'analyse de programmes OCaml
Directeur de thèse:
Antoine MINE (LIP6)
Encadrant :
Raphael MONAT (Inria Lille)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Modèles de calcul, preuve, vérification
Resumé: Le but de cette thèse est de développer, prouver correctes et implanter des nouvelles analyses statiques sémantiques pour vérifier des programmes écrits dans des langages fonctionnels.
Sur le plan théorique, le cadre de l'interprétation abstraite sera utilisé, tandis que sur le plan pratique, l'implantation et les expérimentations seront réalisées au sein de la plateforme d'analyse statique MOPSA, en ciblant l'analyse des programmes OCaml.
L'analyse statique permet de déterminer automatiquement et dès la compilation des propriétés des exécutions des programmes informatiques.
En particulier, les analyses statiques de valeurs déterminent l'ensemble des valeurs possibles des variables, ce qui permet de s'assurer de l'absence de certaines classes importantes d'erreurs (dépassements de capacité, débordements de tableaux, exceptions non rattrapées, ...) et de vérifier qu'un programme obéit à une spécification.
L'analyse de valeurs par interprétation abstraite a été appliquée avec succès à l’analyse de langages impératifs, comme le C, et de langages orientés objet, comme Java.
Il existe encore peu de travaux sur l'analyse de valeurs à des fins de vérification pour les langages fonctionnels.
Le sujet de cette thèse cible les langages fonctionnels strictement typés « à la ML », tel que le langage OCaml.
Le travail comportera des aspects théoriques (développement de sémantiques, d'abstractions, de preuves de correction) ainsi que des aspects pratiques (implantation des abstractions, analyse d'un sous-ensemble non-trivial d'OCaml, expérimentation, évaluation de la qualité des résultats obtenus et des limites des abstractions développées).
L'état de l'art présente des domaines abstraits pour représenter des types algébriques.
Cependant, il s'agit de premières propositions, dont le coût et la précision ont été peu étudiés dans le cadre d'analyses réalistes.
Un premier travail sera donc d'évaluer ces domaines et de les améliorer si nécessaire.
Un deuxième travail sera de développer des domaines abstraits novateurs capables de raisonner sur les types paramétrés afin de gérer efficacement le polymorphisme paramétrique.
Un troisième travail sera la gestion de l'ordre supérieur. Une piste intéressante serait de développer des domaines capables de résumer directement l'effet d'un appel de fonction d'ordre supérieur tout en restant paramétrés par des abstractions numériques et en traitant les types paramétrés. Cette thématique se rapproche de l'analyse modulaire par interprétation abstraite.
Au delà des propriétés de sûreté non-fonctionnelle (comme l'absence de débordements d'entiers et de tableaux, ou d'exceptions non rattrapées), la thèse pourra également considérer la preuve de propriétés fonctionnelles.
Finalement, si le temps le permet, des extensions sont possibles pour supporter les constructions impures d'OCaml ainsi que les foncions C natives.
Pour toutes ces pistes de recherche, les solutions retenues devront être bien définies formellement et devront également être motivées par l'analyse de cas d’étude représentatifs de programmes OCaml réels.
Les résultats de cette thèse devraient aboutir au développement d'analyseurs statiques par interprétation abstraite originaux, pour des propriétés et des langages qui ne sont pas ou peu actuellement considérés par l'état de l'art.
La thèse peut avoir un impact important sur l'amélioration de la sûreté de fonctionnement des logiciels, et sur l'évolution des pratiques de développement et de vérification des logiciels.
Doctorant.e: Valnet Milla