Lecture | Topic | Course Material | Handins |
---|---|---|---|
Chapter 1 | Course intro + Basic concepts of abstract interpretation |
Abstract Interpretation in a Nutshell Cousot-Cousot:BIS04, corresponding slides (90 min) Slides from the lecture |
Handin 1 |
Chapter 2 | Operational semantics: transition system semantics for 3CM and IMP + Collecting semantics, revisited |
Plotkin:TR81 chap. 1 (PostScript file) Slides from the lecture Siveroni:JLAP04 (optional) |
No handin |
Chapter 3 | Concepts of abstract interpretation I Calculating a three counter machine analysis I |
Cousot-Cousot:JLP92, p.1-18
(Sec.7-10 optional) Slides from the lecture Calculation of 3 counter machine analysis, part 1 Implementation of Plotkin's 3 counter machine |
Handin 2 |
Chapter 4 | Concepts of abstract interpretation II Calculating a three counter machine analysis II |
Cousot-Cousot:JLP92, p.18-39
(Sec.7-10 optional) Slides from the lecture Calculation of 3 counter machine analysis, part 2 |
No handin |
Chapter 5 | Numeric and structural abstractions | Miné:thesis,
Sec. 2.4.5 - 2.5 Deutsch:POPL90 Sec. 2 (the rest is optional) Slides from the lecture Link: A graphical overview of a number of numerical abstractions Cousot-Cousot:ICCL94 (optional,however a treasure chest of Galois connections) |
Handin 3 |
Chapter 6 | Case studies: Abstract Debugging of Higher-Order Imperative Languages, Context-Sensitive Analysis of Obfuscated x86 Executables, and The ASTRÉE Static Analyzer |
Bourdoncle:PLDI93 Lakhotia-al:PEPM10 HOSC11 Blanchet-al:PLDI03 Slides-1 from the lecture Slides-2 from the lecture Slides from Lakhotia-al's PEPM'10 presentation Slides from Blanchet-al's PLDI'03 presentation Blanchet-al:Jones-festschrift02 (optional) |
Project description |
En contrôle continu, un partiel écrit 50% + un exposé 50%.
Présenter un outil de rise4fun lors de la dernière séance de cours, un étudiant par exposé, 15 minutes, transparents en français, démo éventuelle.