Grading/Homework/Exam

The course grading will be split into project and exam, possibly replaced with homework (depending on the conditions). Homework, projects, and their deadline will be announced here.

Final grades will be the average of the project grade and of the exam (or 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 in room Emile Noether (occasionally, lessons may be taught online with 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, 11 February 2022: Introduction. (Xavier Rival).
• Lesson 2, 18 February 2022: Operational Semantics (Xavier Rival).
• Lesson 3, 25 February 2022: Trace Properties (Xavier Rival).
• Lesson 4, 11 March 2022: Denotational Semantics (Jérôme Feret).
• Lesson 5, 18 March 2022: Axiomatic semantics (Jérôme Feret).
• Lesson 6, 25 March 2022: Types (Jérôme Feret).
• Lesson 7, 1 April 2022: The Coq proof assistant. (Josselin Giet and Xavier Rival).
• Lesson 8, 8 April 2022: Résolution Modulo Théorie (SMT) (Josselin Giet).
• Lesson 9, 15 April 2022: Abstract interpretation I (Xavier Rival).
• Lesson 10, 22 April 2022: Abstract interpretation II (Xavier Rival).
• Lesson 11, 13 May 2022: Abstract interpretation III (Jérôme Feret).
• Lesson 12, 20 May 2022: Abstract interpretation IV (Jérôme Feret).
• Exam: 27 May 2022 or 3 June 2022.

Lab sessions

The material of the lab sessions will be added soon.

Projects

Information on the project will be announded at a later date.

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 2020-2021 can be found here.
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.