Semantics and applications to verification
Sylvain Conchon, Antoine Miné and Xavier Rival
L3, École Normale Supérieure
Exam
The exam will take place in Salle UV, at École Normale Supérieure, on Friday 3rd of June, from 10h00 till 12h00.
Organization
The course takes place in Salle UV, at École Normale Supérieure, on Friday mornings, from 8h30 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, 12 February 2016: Introduction (Xavier Rival).
- Lesson 2, 19 February 2016: Operational Semantics (Xavier Rival).
- Lesson 3, 26 February 2016: Trace Properties (Xavier Rival).
- Lesson 4, 4 March 2016: Denotational Semantics (Antoine Miné).
- Lesson 5, 11 March 2016: Types (Antoine Miné).
- Lesson 6, 18 March 2016: Axiomatic semantics (Antoine Miné).
- Lesson 7, 25 March 2016: The Coq proof assistant (Xavier Rival).
- Lesson 8, 1 April 2016: Model-Checking Modulo Theories (Sylvain Conchon).
- Lesson 9, 8 April 2016: Satisfiability Modulo Theories (Sylvain Conchon).
- Lesson 10, 15 April 2016: Abstract interpretation I (Xavier Rival).
- Lesson 11, 13 May 2016: Abstract interpretation II (Antoine Miné).
- Lesson 12, 20 May 2016: Abstract interpretation III (Antoine Miné).
- Lesson 13, 27 May 2016: Abstract interpretation IV (Antoine Miné).
- Lesson 14, 3 June 2016: Written exam.
Lab Sessions
The lab sessions are found here.
Projects
Two project topics are proposed:
The projects should be finished and submitted by the 3rd of June 2016 (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 2013-2014 can be found here.
The webpage of the course of year 2014-2015 can be found here.
Exams of the previous year
The exam of the course of year 2013-2014 can be found here.
The exam of the course of year 2014-2015 can be found here.