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

  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

Pré-requis