Laboratoire: Verimag (http://www-verimag.imag.fr/)
Équipe: SYNCHRONE (http://www-verimag.imag.fr/SYNCHRONE)
Encadrants: David Monniaux <David.Monniaux@imag.fr>, Matthieu Moy <Matthieu.Moy@imag.fr> et Julien Henry <Julien.Henry@imag.fr>.
Contexte Scientifique
L’analyse de programmes par interprétation abstraite calcule de façon sûre des propriétés vraies pour toutes les exécutions de programmes, à l’aide de représentations symboliques (polyèdres convexes, formules de logique, automates finis..) de sur-ensembles des états possibles du programme. La difficulté consiste à garder une bonne précision (obtenir des petits invariants, permettant de démontrer les propriétés désirées) tout en gardant une bonne complexité (temps et espace), sachant que les problèmes considérés sont souvent indécidables ou NP-durs.
Ces dernières années ont été développées des techniques augmentant la précision des analyses en distinguant les chemins dans le programme [M_LMCS10, GH_ESOP11, MG_SAS11, HMM_SAS12]; afin d’éviter des énumérations exponentielles inutiles, elles s’appuient sur les tests de satisfiabilité modulo théorie (SMT), dont des versions efficaces sont arrivées pendant les années 2000.
Un outil d’interprétation abstraite pour des programmes écrits en C ou C++ est développé à Verimag, et implémente plusieurs de ces techniques, ainsi qu’une nouvelle technique qui les combine. Cet analyseur permet de comparer ces techniques sur des programmes de grande taille, pour savoir quelle analyse se comporte le mieux en pratique.
Sujet
Il y a de très nombreuses directions possibles d’amélioration, à la fois de l’état de l’art scientifique et de ce qui est implémenté dans notre outil. L’étudiant pourra s’intéresser, suivant les goûts, à :
- Une analyse plus raffinée des programmes avec pointeurs ou tableaux
- Une meilleure gestion des relations entre les variables booléennes et numériques
- De meilleures heuristiques de parcours du graphe de flot de controle du programme
- Une meilleure utilisation du SMT-solveur, en simplifiant la formule à résoudre avant de lancer le solveur
- Une meilleure gestion des nombres flottants
- ou tout autre aspect qui mérite amélioration !
L’étudiant commencera par se familiariser avec l’interprétation abstraite en général, et l’outil Verimag en particulier, puis choisira un ou plusieurs des points ci-dessus. Ces fonctionalités seront conçues, implémentées, puis testées sur les benchmarks existants.
Compétences Attendues
- De bonnes bases en informatique théorique (la connaissance de l’interprétation abstraite n’est pas nécessaire mais serait un plus)
- Des notions de compilation (l’outil d’analyse utilise LLVM)
- C++
Contexte de Travail
Le stagiaire travaillera en étroite collaboration avec Julien Henry (doctorant) sur la partie implémentation, et sera encadré par David Monniaux et Matthieu Moy (permanents du laboratoire).
