Description
The description of this lecture can be found on the SIF master webpage.
Teachers
Thomas
Jensen (TJ)
and Benoît
Montagu (BM)
Guest lecture
by Benjamin
Farinier (BF)
Evaluation
A quiz (exam) on the first part of the course and student presentations (groups of two) of articles from the research literature.
Planning, lecture notes
Lectures take place on Tuesdays 8:00 - 9:30 and Wednesdays 15:00 - 16:30.
| Lecture | Date | Topic | Teacher | Handout |
|---|---|---|---|---|
| 1 | 11/09/2024 | Operational semantics | BM | [slides] [handout] |
| 2 | 17/09/2024 | Operational semantics | TJ | slides |
| 3 | 18/09/2024 | Type systems | TJ | |
| 4 | 24/09/2024 | Data flow analysis | TJ | slides |
| 5 | 25/09/2024 | Data flow analysis | TJ | |
| 6 | 01/10/2024 | Abstract interpretation | TJ | slides |
| 7 | 02/10/2024 | Abstract interpretation | TJ | |
| 8 | 08/10/2024 | Control flow analysis | BM | [slides] [handout] |
| 9 | 9/10/2024 | Control flow analysis | BM | [OCaml source code] |
| 10 | 15/10/2024 | Information flow analysis | TJ | slides |
| 11 | 16/10/2024 | Information flow challenge | slides | |
| 12 | 22/10/2024 | Symbolic execution | BF | |
| 13 | 23/10/2024 | Quiz | BM, TJ | |
| 29/10/2024 | Fall break | |||
| 30/10/2024 | Fall break | |||
| 14 | 4-8/11/2024 | Preparation of student presentations | ||
| 15 | 12-13/11/2024 | Student presentations | BM, TJ |
Student presentations
- Separation logic: Local Reasoning about Programs that Alter Data Structures (O'Hearn, Reynolds, Yang) (Informal description of separation logic)
- A Few Graph-Based Relational Numerical Abstract Domains (Miné)
- On flow-sensitive Security Types (Hunt, Sands)
- System-level non-interference for constant-time cryptography (Barthe et al.)
- Precise static analysis of untrusted driver binaries (Kinder, Veith)
Student presentation will take place on Wednesday November 13th from 14:00 to 16:00 in room B12D i57.
| Students | Articles |
| Samuel Hiron Jad Zahreddine |
Precise static analysis of untrusted driver binaries |
| Alban Dutilleul Martin Andrieux |
Local Reasoning about Programs that Alter Data Structures |
| Pierre Nunn Thomas Feuilletin |
A Few Graph-Based Relational Numeric Abstract Domains |
| Sarah Emery Valentin Hautiquet |
System-level non-interference for constant-time cryptography |
| Baptiste Amice Grégory Brivady |
Local Reasoning about Programs that Alter Data Structures |