Semantics and applications to verification
Sylvain Conchon, Jérôme Feret and Xavier Rival
L3, École Normale Supérieure
The exam will take place in Salle UV, at École Normale Supérieure, on Friday 2nd of June, from 10h00 till 12h00.
The course takes place in Salle UV, at École Normale Supérieure, on Friday mornings, from 8h30 till 12h15.
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.
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, 3 February 2017: Introduction (Xavier Rival).
- Lesson 2, 10 February 2017: Operational Semantics (Xavier Rival).
- Lesson 3, 17 February 2017: Trace Properties (Xavier Rival).
- Lesson 4, 24 February 2017: The Coq proof assistant (Xavier Rival).
- Lesson 5, 10 March 2017: Denotational Semantics (Jérôme Feret).
- Lesson 6, 17 March 2017: Types (Jérôme Feret).
- Lesson 7, 24 March 2017: Axiomatic semantics (Jérôme Feret).
- Lesson 8, 21 April 2017: Model-Checking Modulo Theories (Sylvain Conchon).
- Lesson 9, 28 April 2017: Satisfiability Modulo Theories (Sylvain Conchon).
- Lesson 10, 5 May 2017: Abstract interpretation I (Xavier Rival).
- Lesson 11, 12 May 2017: Abstract interpretation II (Xavier Rival).
- Lesson 12, 19 May 2017: Abstract interpretation III (Jérôme Feret).
- Lesson 13, 26 May 2017: Abstract interpretation IV (Jérôme Feret).
- Lesson 14, 2 June 2017: Written exam.
Two project topics are proposed:
The projects should be finished and submitted by the 10th of June 2017 (same date as for the written exam) (anywhere on earth). Students may complete the project individually, or by group of two. The submitted version should include source code (with comments), test cases and a report.