---

Cette page concerne la deuxième moitié du cours Typage et analyse statique, c'est à dire la partie analyse statique (cours 8 à 14).

Planning prévisionnel

Le cours commence jeudi 9 février à 8h30 et a lieu en salle STL.
Il dure 2h et est suivi d'une séance de TME de 2h en salle STL.

Supports de cours

• 09/02/17 : Cours 8
• 16/02/17 : Cours 9
• 23/02/17 : Cours 10
• 02/03/17 : Cours 11
• 09/03/17 : Cours 12
• 16/03/17 : Cours 13
• 23/04/17 : Cours 14

Projet

Projet en binôme, à commencer en TME à partir des sources de base et à finir chez soi pour un rendu le jour de l'examen final.

• énoncé du projet
• image VirtualBox pré-installée avec les sources de base du projet (2.5 GB)
• alternativement : sources de base du projet seules pour Linux, voir le fichier INSTALL.TXT pour les dépendances

Examen final et présentation orale

L'examen final prendra la forme d'une présentation orale en binôme d'un article scientifique le 30 mars 2017, à choisir dans la liste ci-dessous.

Indiquez votre choix d'article ainsi que votre nom et celui de votre binôme par email à

La présentation durera 15mn et sera suivie de 10mn de questions. Vous devrez obligatoirement préparer des transparents (de préférence au format PDF). Dans une présentation en binôme, les deux membres du binôme devront présenter à part égale et répondre aux questions.

1. Static analysis of list-manipulating programs via bit-vectors and numerical abstractions. Liqian Chen, Renjian Li, Xueguang Wu, Ji Wang. In: Symposium On Applied Computing (SAC 2013).
2. Taming the wrapping of integer arithmetic. Axel Simon, Andy King. In: Static Analysis Symposium (SAS 2007).
3. Lookahead Widening. Denis Gopan, Thomas Reps. In: Computer Aided Verification (CAV 2006).
4. Trace partitioning in abstract interpretation based static analyzers. Laurent Mauborgne, Xavier Rival. In: European Symposium on Programming (ESOP 2015).
5. Abstract interpretation of microcontroller code: Intervals meet congruences. Jörg Brauer, Andy King, Stefan Kowalewski, In Sci. Comput. Program (2013).
6. Discovering properties about arrays in simple programs. Nicolas Halbwachs and Mathias Péron. In: Programming Languages Design and Implementation (PLDI 2008).
7. Static analysis of string manipulations in critical embedded C programs. Xavier Allamigeon, Wenceslas Godard, Charles Hymans. In: Satic Analysis Symposium (SAS 2006).
8. Interval slopes as a numerical abstract domain for floating-point variables. Alexandre Chapoutot. In: Static Analysis Symposium (SAS 2010).
9. Automatic repair of overflowing expressions with abstract interpretation. Francesco Logozzo, Matthieu Martel. In: Festschrift for Dave Schmidt, 2013.
10. Widening for control flow. Ben Hardekopf, Ben Wiedermann, Berkeley Churchill, Vineeth Kashyap. In: Verification, Model Checking, and Abstract Interpretation (VMCAI 2014).
11. A policy iteration algorithm for computing fixed points in static analysis of programs. Alexandru Costan, Eric Goubault, Stéphane Gaubert, Matthieu Martel, Sylvie Putot. In: Computer Aided Verification (CAV 2005).
12. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. Francesco Logozzo, Manuel Fähndrich. In: Science of Computer Programming, Sept. 2010, Vol 75, Issue 9.
13. Deriving numerical abstract domains via principal component analysis. Gianluca Amato, Maurizio Parton, Francesca Scozzari. In: Static Analysis Symposium (SAS 2010).
14. The abstract domain of parallelotopes. Gianluca Amato, Francesca Scozzari. In: Numerical and Symbolic Abstract Domains (NSAD 2012).
15. A framework for numeric analysis of array operations. D. Gopan, T. Reps, M. Sagiv. In: Principles of Programming Languages (POPL 2005).
16. Combining widening and acceleration in linear relation analysis.Laure Gonnord, Nicolas Halbwachs. In: Static Analysis Symposium (SAS 2006).
17. The Octahedron abstract domain. Robert Clarisé, Jordi Cortadella. In: Static Analysis Symposium (SAS 2004).
18. Analyzing memory accesses in x86 executables. Gogul Balakrishnan, Thomas Reps. In: Compiler Construction (CC 2004).
19. Verification of device drivers and intelligent controllers: a case study. David Monniaux. In: EMSOFT 2007.
20. String analysis for dynamic field access. Magnus Madsen, Esben Andreasen. In: Compiler Construction (CC 2014).
21. When the decreasing sequence fails. Nicolas Halbwachs, Julien Henry. In: Static Analysis Symposium (SAS 2012).

Ressources externes

Quelques ressources utiles concernant l'analyse statique par interprétation abstraite :

• Présentation de Patrick Cousot au Colloquium de l'UPMC (en anglais).
• Présentation de Patrick Cousot au Collège de France.