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).
Sujet
Créer et implémenter des analyses permettant de considérer des programmes utilisant des structures de données (listes, arbres, etc.).
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
- C++ ou Caml
Contexte de Travail
Le stagiaire sera encadré par David Monniaux et Matthieu Moy (permanents du laboratoire) et travaillera éventuellement en collaboration avec Julien Henry (doctorant) sur la partie implémentation.
