Vérification statique

Une application notable : Astrée

Cours

Conception et rédaction du cours original : Jan Midtgaard.

Organisation

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

Evaluation

En contrôle continu, un partiel écrit 50% + un exposé 50%.

Sujets d'exposés

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.

Autres ressources


Valid HTML5