L'analyse statique consiste à raisonner sur le comportement des programmes informatiques sans avoir à les exécuter. Cette technique est utilisée dans les compilateurs optimisants, afin de générer du code efficace à partir de propriétés du code inférées par l'outil. C'est également utilisé pour la détection automatique d'erreurs, afin d'aider les programmeurs à écrire de meilleurs programmes et moins de tests. Ce module enseigne à la fois la théorie et la pratique : à la fin du semestre, vous aurez implémenté une analyse de flot de donnée ainsi qu'une analyse par interprétation abstraite, ainsi que quelques analyses dans chacun de ces outils.

1. Fondations
   • Théorie des ordres
   • Résultats sur les points fixes
   • Le langage WHILE
2. Analyse de flot de données
   • Essence des compilateurs optimisant (GCC, Clang, etc.)
   • Objectif : implémenter une analyse
3. Interprétation abstraite
   • Essense des outils d'analyse statique (Infer, AbsInt, Frama-C, etc.)
   • Objectif : implémenter un interpréteur abstrait

• Cours Programmation Fonctionnelle du L3 :
  • Programmation fonctionnelle en OCaml
  • Programmer avec des structures de données algébriques (arbres) en OCaml
  • Utilisation basique des modules en OCaml (fichiers séparés pour interface et réalisation d'un module)
  • Compilation d'un projet OCaml consistant de plusieurs modules pour créer un exécutable autonome, en utilisant une des techniques comme dune, ocamlbuild, make, …

• Cours Programmation C ou Java du L2 :
  • Programmation impérative
  • Sémantique des structures de contrôle impératives (conditionnelles, boucles)
  • Notion d'invariant de boucle