Différences

Ci-dessous, les différences entre deux révisions de la page.

--- formations:masters:ue:m2:astat10 [2023/04/21 09:12] – supprimée - modification externe (Unknown date) 127.0.0.1
+++ formations:masters:ue:m2:astat10 [2023/04/21 09:12] (Version actuelle) – ↷ Page déplacée de formations:masters:cours:m2:astat10 à formations:masters:ue:m2:astat10 treinen
@@ Ligne 1: / Ligne 1: @@
+~~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

Outils pour utilisateurs

Outils du site

Différences

Outils de la page