~~NOTOC~~

====== Analyse Statique ======

===== Description =====

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.

===== Syllabus =====

==== Sujets centraux ====

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

===== Pré-requis =====

  * 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