L’analyse automatique de programmes permet de démontrer l’absence de certains problèmes (p.ex. débordements de tableaux, dépassements arithmétiques) avant de lancer effectivement les programmes, ce qui est précieux pour certaines applications (p.ex. aéronautique). Elle diffère du test en ce que le test ne vérifie qu’un nombre fini de cas et peut donc laisser passer des problèmes.
Une des difficultés pour analyser des programmes de grande taille est la croissance du coût (temps, mémoire) des algorithmes d’analyse avec la taille du code et le nombre de variables. Pour conserver des coûts tolérables, il est nécessaire de procéder modulairement : réaliser des analyses sur des parties du programmes assez indépendamment les unes des autres.
Certaines techniques modulaires se basent sur des limites syntaxiques du programme source : on va analyser fonction par fonction, classe par classe, etc. Ces critères sont peu pertinents dans le cas de certains types de logiciels, notamment ceux de contrôle synchrone tels qu’utilisés en avionique, où ce seraient plutôt des réseaux de dépendances entre variables qui devraient être étudiés. L’objet du stage est de concevoir, étudier et implanter des heuristiques de découpage modulaire.
Compétences demandées :
- notions de logique mathématique
- notions de compilation
- programmation en Objective Caml (Java ou C++ possibles)
Travail attendu : conception de méthodes d’analyse modulaire implantation dans un outil
Ce sujet pourra se poursuivre en thèse (des financements sont prévus dans le cadre du projet ERC STATOR). Contacter : David Monniaux, laboratoire VERIMAG <David.Monniaux>
