Stage : Analyses statiques pour le langage Rust

Analyses statiques pour le langage Rust

Le langage Rust est un langage système proposant des constructions modernes et de haut niveau comme le filtrage de motif, les fermetures, les génériques, etc. Il se distingue aussi par l'introduction, en complément d'une analyse de type, d'une vérification statique de propriétés liées à l'utilisation sûre de la mémoire dans les programmes. Dans ce stage, nous souhaitons étudier les possibilités d'analyses statiques complémentaires, et basées sur des techniques d'interprétation abstraite. Le stage comprendra une partie plus théorique, en particulier la formalisation d'une sémantique formelle pour un sous-ensemble non trivial du langage Rust. Il comprendra également une partie plus pratique, avec le développement d'un prototype d'analyseur statique "simple".

Le stagiaire devra être d'accord pour que ses contributions soient développées et distribuées sous licence libre.

Le stage sera encadré par Antoine Miné et Frédéric Peschanski (LIP6) Contact : Frederic.Peschanski@lip6.fr