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 le très grand nombre de chemins possibles dans le code : soit on « mélange » des résultats d’analyse de chemins différents (ce qui peut donner des résultats décevants et empêcher de démontrer des propriétés pourtant vraies), soit on les traite séparément, ce qui peut être très coûteux. Heureusement, dans la dernière décennie, des algorithmes de décision rapides ont été développés. L’objectif de ce stage est de les exploiter au mieux.
Il s’agit d’introduire des procédures de décision dans la résolution de certains problèmes (calcul d’invariants par itération de politique, calcul de variants pour prouver la terminaison...) pour lesquels les algorithmes précédemment connus procèdent par énumération explicite des chemins. Les techniques seront implantées effectivement, le plus simple étant probablement de les rajouter dans l’outil PAGAI http://www-verimag.imag.fr/Pagai.html
Compétences demandées :
- notions de logique mathématique
- notions de compilation
- notions de programmation linéaire
- programmation en C++ et/ou Objective Caml
Travail attendu : amélioration des méthodes déjà proposées (Gawlitza & Monniaux, ESOP 2011) ou en cours de développement implantation dans un outil capable de passer sur des programmes réels
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>
