MPRI Course 2-36-1: Proof of Program

This page presents teaching material for Course 2-36-1 "Proof of Program" of the MPRI 2014-2015.

Organisation

• Location: bâtiment Sophie Germain, room 1009.
• Time: Thursday, 16:15 to 19:15.
• First course: December 11th.
• Project due: Extended dead-line: February 23th at 19:00 UTC+1.
• Exam: March 12th, 16:15 to 19:15.

Remark: there will be no course on January 8th and March 5th.

Exam -- New

You may have a look at the exam of 2014. Once you have solved all exercises (and not before!), you may check some of the solutions.

Note that there will be no questions on characteristic formulae.

Project

The project was provided on December 18th.

It will consist of a formal development using Why3 and automated provers.

To install Why3 and the automated provers, follow the installation procedure.

The project consists of the formalization of two-player games. Here is the canvas file provided.

Lectures

Slides and examples will be posted here. [Warning: dates to be confirmed.]

Part 1: Program verification using Hoare Logic, lectured by Claude Marché.

• Lecture 1 (December 11th): Basics of deductive program verification.
  • Covers: classical Hoare logic, partial/total correctness, weakest liberal preconditions, blocking semantics, examples with Why3 and SMT solvers.
  • Slides
  • Running example in Why3: ISQRT
  • Canvas for exercises: Exercise 1, Exercise 2, Exercise 3
• Lecture 2 (December 18th): More advanced topics in program verification
  • Covers: blocking semantics continued, treatment of local variables, ghost variables and labels, function calls and modularity aspects, termination, specification languages, lemma functions.
  • Slides
  • Solutions to exercices of lecture 1: Euclide's algorithm, Fast exponentiation
  • Examples in Why3: Euclide with ghost variables, Euclide with labels,
  • Exercises: Bezout coefficients, McCarthy's 91 function Lemma functions
• Lecture 3 (January 15th): Handling of data structures
  • Covers: products and sum types, lists ; specification using abstract types, sets, maps, arrays; exceptions ; computer arithmetic.
  • Slides
  • Solutions to exercices of lecture 2: Bezout coefficient, McCarthy 91 function, Lemma functions,
  • Examples in Why3 or C: List reversal, Linear search, Linear search with an exception, Exact square root, with an exception, arith.c, bin_search_int32.c, bin_search.c, clock_drift.c,
  • Exercises: Binary Search
• Lecture 4 (January 22th): Aliasing issues
  • Covers: call by reference, alias control by static typing ; inductive predicates ; component-as-array modeling for pointer programs.
  • Slides
  • Solutions to exercices of lecture 3: Binary search
  • Examples in Why3: Stack part 1, Stack part 2, Selection sort In place linked-list reversal
  • Exercises: In-place linked-list concatenation
• Answering questions related to the project (one week in February)

Part 2: Separation Logic and representation predicates, lectured by Arthur Charguéraud.

• All lectures, for printing:
  • Slides of Part 1 to 4, with 4 slides per page
  • Slides of Part 1 to 4, with 1 slide per page
• Lecture 5 (January 29th): Separation Logic 1
  • Covers: Separation Logic heap predicates and triples, mutable lists
  • Slides of introduction
  • Slides of Part 1 and printable version
  • Exercises and solutions are provided at the end of the slides.
• Lecture 6 (February 5th): Separation Logic 2
  • Covers: list segments, mutable trees, reasoning rules
  • Slides of Part 2 and printable version
  • Exercises and solutions are provided at the end of the slides.
• Lab session (February 12th): help on the project
• Lecture 7 (February 19th): Separation Logic 3
  • Covers: loops, soundness theorem, higher-order functions, deallocation, concurrency
  • Slides of Part 3 and printable version
  • Exercises and solutions to proofs are provided at the end of the slides.
• Lecture 8 (February 26th): Separation Logic 4
  • Covers: arrays, polymorphic representation predicates, recursive ownership, characteristic formulae
  • Slides of Part 4 and printable version
  • Exercises and solutions to proofs are provided at the end of the slides.
• All lectures, for printing: see above.

Past versions

• Course given in 2013-2014
• Course given in 2012-2013 (different content)
• Course given in 2011-2012 (different content)