Organization

The course takes place in Salle R, at École Normale Supérieure, on Wednesday afternoons, from 14h (2PM) till 17h30 (5.30PM).

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 0, 12 February 2014: Introduction (Xavier Rival).
• Lesson 1, 19 February 2014: Operational Semantics (Xavier Rival).
• Lesson 2, 26 February 2014: Denotational Semantics (Antoine Miné).
• Lesson 3, 5 March 2014: Types (Antoine Miné).
• Lesson 4, 12 March 2014: Axiomatic semantics (Antoine Miné).
• Lesson 5, 19 March 2014: Trace properties (Xavier Rival).
• Lesson 6, 26 March 2014: Semantic equivalence The Coq proof assistant (Xavier Rival).
• Lesson 7, 2 April 2014: Model-Checking Modulo Theories ex2.cub ex3.cub mut_loc.cub bakery_uguard.cub (Sylvain Conchon).
• Lesson 8, 9 April 2014: Satisfiability Modulo Theories (Sylvain Conchon).
• Lesson 9, 30 April 2014: Abstract interpretation I (Xavier Rival).
• Lesson 10, 7 May 2014: Abstract interpretation II (Antoine Miné).
• Lesson 11, 14 May 2014: Abstract interpretation III (Antoine Miné).
• Lesson 12, 21 May 2014: Abstract interpretation IV (Antoine Miné).
• Lesson 13, 28 May 2014: written exam.

Lab Sessions and Project

The lab sessions are found here. The project is described here.