Description
Date depot: 10 mars 2019
Titre: Analyse statique par interprétation abstraite de la portabilité des logiciels
Directeur de thèse:
Antoine MINE (LIP6)
Domaine scientifique: Sciences pour l'ingénieur
Thématique CNRS : Non defini
Resumé:
Le but de la thèse est de développer des nouvelles classes d'analyses statiques qui soient adaptées aux propriétés de portabilité, en particulier pour évaluer l'impact d'un changement de l'environnement sur la sémantique d'un programme.Les logiciels informatiques tendent à être utilisés beaucoup plus longtemps et dans une plus grande variété d'environnements que prévu lors de leur conception. Si aucune précaution n'est prise, l'adaptation d'un logiciel à de nouvelles utilisations peut s'avérer très difficile et coûteuse. Assurer la portabilité des programmes est un enjeu majeur : il s'agit de s'assurer que leur compilation et leur exécution dans un environnement différent aura un effet réduit et maîtrisé sur leur sémantique, et que la sûreté d'exécution n'est pas compromise.Afin de vérifier les logiciels, les méthodes de test, encore majoritairement employées dans l'industrie, sont de plus en plus souvent complétées par des méthodes formelles, qui offrent des garanties mathématiques sur la correction, en particulier les outils basés sur l'interprétation abstraite. Pour la plupart, ces analyseurs ne savent pas prendre en compte les évolutions de l'environnement de compilation et d'exécution : celui-ci reste figé, et l'analyse doit être relancée à chaque changement de l'environnement. Par ailleurs, les résultats de telles analyses séparées mettent difficilement en évidence les relations entre environnement et sémantique du programme. Les analyses de portabilité garanties formellement n'ont fait leur apparition que très récemment, et restent limitées à des cas particuliers. Ces travaux souffrent de limitations liées à l'emploi de techniques de type solveur SMT ou exécution symbolique, qui rendent difficile le traitement des boucles en garantissant la terminaison de l'analyse, alors que ce problème est bien traité par les méthodes à base d'interprétation abstraite. Le sujet de thèse proposé ici est ancré dans la problématique de l'analyse statique par interprétation abstraite pour des propriétés de portabilité, et vise à construire des analyses plus générales et plus matures que l'état de l'art.Le travail pourra explorer en particulier les pistes suivantes : la spécification formelle des propriétés de portabilité, les domaines abstraits pour l'analyse de portabilité, les analyses différentielles sur l'environnement, les analyses différentielles sur le code, la validation théorique et expérimentale.Les résultats de cette thèse devraient aboutir au développement d'analyseurs statiques originaux, pour des propriétés qui ne sont pas actuellement considérées 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: Delmas David