Semantics and applications to verification
Course:
Sylvain Conchon, Jérôme Feret and Xavier Rival
L3, École Normale Supérieure
TDs: Marc Chevalier
Exam
The exam will take place in Salle R, at École Normale Supérieure, on Friday 31st of May, from 10h00 till 12h00.
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, 8 February 2019: Introduction (Xavier Rival).
- Lesson 2, 15 February 2019: Operational Semantics (Xavier Rival).
- Lesson 3, 22 February 2019: Trace Properties (Xavier Rival).
- Lesson 4, 1 March 2019: The Coq proof assistant (Xavier Rival).
- Lesson 5, 8 March 2019: Denotational Semantics (Jérôme Feret).
- Lesson 6, 15 March 2019: Types (Jérôme Feret).
- Lesson 7, 22 March 2019: Axiomatic semantics (Jérôme Feret).
- Lesson 8, 29 March 2019: Model-Checking Modulo Theories (Sylvain Conchon).
- Lesson 9, 5 April 2019: Satisfiability Modulo Theories (Sylvain Conchon).
- Lesson 10, 19 April 2019: Abstract interpretation I (Xavier Rival).
- Lesson 11, 10 May 2019: Abstract interpretation II (Xavier Rival).
- Lesson 12, 17 May 2019: Abstract interpretation III (Jérôme Feret).
- Lesson 13, 24 May 2019: Abstract interpretation IV (Jérôme Feret).
- Lesson 14, 31 May 2019: Written exam.
Lab sessions
The material of the lab sessions can be accessed here.
Projects
Three project topics are proposed:
- Implementation of a Mini Solver-SMT
- Implementation of a Static Analyzer
- Semantics and analysis in Coq and Coq template
The projects should be finished and submitted by the 1st of June 2018 (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.
Course of the previous years
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 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.