Semantics and applications to verification
Course:
Jérôme Feret and Xavier Rival
L3, École Normale Supérieure
Lab sessions: Josselin Giet
Grading/Homework
The course grading will be split into project and homework. Homework, projects, and their deadline will be announced here.
Final grades will be the average of the project grade and of the homework grade.
Organization
The course takes place on Friday mornings, from 8h30 till 12h15. This comprises a lecture from 8h30 till 10h00 and a lab session or TD from 10h15 till 12h15. The lecture will be taught on GoToMeeting.
Lecture contents
In this lecture, we will study techniques for reasoning about programs, so as to verify correctness properties. We will first set up the foundations of the semantics of programming languages and the notion of program proofs, using Hoare triples. Then, we will formalize various kind of relevant properties (safety, liveness, security). Last, we will focus on approaches for automatic program verification (abstract interpretation based static analysis, model checking of finite systems, solving modulo theory): the inferrence of the proofs is then performed by another computer program.
Schedule and lectures material
You will find here the provisional course plan. The course plan will be updated progressively and the slides of the courses will be put on-line after each course, so, please consult this page regularly.
- Lesson 1, 5 February 2021: Introduction (Xavier Rival).
- Lesson 2, 12 February 2021: Operational Semantics (Xavier Rival).
- Lesson 3, 19 February 2021: Trace Properties (Xavier Rival).
- Lesson 4, 5 March 2021: Denotational Semantics (Jérôme Feret).
- Lesson 5, 12 March 2021: Axiomatic semantics (Jérôme Feret).
- Lesson 6, 19 March 2021: Types (Jérôme Feret).
- Lesson 7, 26 March 2019: The Coq proof assistant (Xavier Rival).
- Lesson 8, 2 April 2021: Résolution Modulo Théorie (SMT) (TBA).
- Lesson 9, 9 April 2021: Abstract interpretation I (Xavier Rival).
- Lesson 10, 16 April 2021: Abstract interpretation II (Xavier Rival).
- Lesson 11, 7 May 2021: Abstract interpretation III (Jérôme Feret).
- Lesson 12, 14 May 2021: Abstract interpretation IV (Jérôme Feret).
Lab sessions
The material of the lab sessions will be added here soon.
References
The material provided by the class is meant to be self-contained. However, the following references will allow to study more in detail importants part of the course:
- Patrick Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. MFPS 1997: 77-102
- Bowen Alpern and Fred B. Schneider. Recognizing Safety and Liveness. In Distributed Computing, Springer, 1987.
- Patrick Cousot. The Calculational Design of a Generic Abstract Interpreter. In Broy, M., and Steinbrüggen, R. (eds.): Calculational System Design. NATO ASI Series F. Amsterdam: IOS Press, 1999.
- Xavier Rival and Kwangkeun Yi. Static Analysis: an Abstract Interpretation Perspective. MIT Press 2020.
Course of the previous years
The webpage of the course of year 2019-2020 can be found
here.
The webpage of the course of year 2018-2019 can be found
here.
The webpage of the course of year 2017-2018 can be found
here.
The webpage of the course of year 2016-2017 can be found
here.
The webpage of the course of year 2015-2016 can be found
here.
The webpage of the course of year 2014-2015 can be found
here.
The webpage of the course of year 2013-2014 can be found
here.
Exams of the previous years
The exam of the course of year 2018-2019 can be found
here.
The exam of the course of year 2017-2018 can be found
here, and the answers
are here.
The exam of the course of year 2016-2017 can be found
here, and the answers
are here.
The exam of the course of year 2015-2016 can be found
here.
The exam of the course of year 2014-2015 can be found
here.
The exam of the course of year 2013-2014 can be found
here.