Exam

The exam will take place in Salle R, at École Normale Supérieure, on Friday 1st of June, 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, 9 February 2018: Introduction (Xavier Rival).
• Lesson 2, 16 February 2018: Operational Semantics (Xavier Rival).
• Lesson 3, 23 February 2018: Trace Properties (Xavier Rival).
• Lesson 4, 2 March 2018: The Coq proof assistant (Xavier Rival).
• Lesson 5, 9 March 2018: Denotational Semantics (Jérôme Feret).
• Lesson 6, 16 March 2018: Types (Jérôme Feret).
• Lesson 7, 23 March 2018: Axiomatic semantics (Jérôme Feret).
• Lesson 8, 30 March 2018: Abstract interpretation I (Xavier Rival).
• Lesson 9, 6 April 2018: Abstract interpretation II (Xavier Rival).
• Lesson 10, 13 April 2018: Model-Checking Modulo Theories (Sylvain Conchon).
• Lesson 11, 4 May 2018: Satisfiability Modulo Theories (Sylvain Conchon).
• Lesson 12, 18 May 2018: Abstract interpretation III (Jérôme Feret).
• Lesson 13, 25 May 2018: Abstract interpretation IV (Jérôme Feret).
• Lesson 14, 2 June 2018: 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 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.