Vérification statique

29h en présentiel.

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
Slides from the lecture
Cousot-Cousot:BIS04, corresponding slides (90 min) (optional)
Handin 1
Chapter 2 Operational semantics: transition system semantics for 3CM +
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
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
Slides from the lecture
A graphical overview of a number of numerical abstractions
Handin 3
Chapter 6 Case study: Abstract Debugging of Higher-Order Imperative Languages Bourdoncle:PLDI93
Slides from the lecture
No handin

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 (a priori le 18 novembre à partir de 13h30), un étudiant par exposé, 15 minutes, transparents en français, démo éventuelle.

Autres ressources


Valid HTML5