Semantics and applications to verification
Course:
Jérôme Feret and Xavier Rival
L3, École Normale Supérieure
TDs: Marc Chevalier
Grading/Homework
A graded homework (devoir maison) will be provided on Tuesday, 19th of May. Submissions will be due by Wednesday, 27th of May.
The exam topic is now available here.
Final grades will be the average of the project grade and of the homework grade.
Organization
The course takes place in Salle R, at École Normale Supérieure, 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.
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, 7 February 2020: Introduction (Xavier Rival).
- Lesson 2, 14 February 2020: Operational Semantics (Xavier Rival).
- Lesson 3, 28 February 2020: Trace Properties (Xavier Rival).
- Lesson 4, 6 March 2020: Denotational Semantics (Jérôme Feret).
- Lesson 5, 13 March 2020: Axiomatic semantics (Jérôme Feret).
- Lesson 6, 20 March 2020: Résolution Modulo Théorie (SMT) (l'ensemble des informations sur la séance ainsi que le TD se trouve ici)
- Lesson 7, 27 March 2020: Abstract interpretation I (Xavier Rival).
- Lesson 8, 3 April 2020: Abstract interpretation II (Xavier Rival).
- Lesson 9, 24 April 2020: Abstract interpretation III (Jérôme Feret).
- Lesson 10, 15 May 2020: Abstract interpretation IV (Jérôme Feret).
- Lesson 11, 22 May 2020: Types (Jérôme Feret).
Lab sessions
The material of the lab sessions can be accessed here.
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 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 year
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.