MPRI Course 2-36-1: Proof of Program

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

Organisation

• Location: bâtiment Sophie Germain, room 1009.
• First course: December 13rd.
• Exam: March 14th, 13:15 to 16:15, room 1009

Remark: there will be no course on January 10th.

Exam

The text of the exam, and a version including some solutions.

Project

The project consists of the formalization of a convex hull algorithm. Here is the canvas file provided.

Lectures

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

• Lecture 1 (December 13th): Basics of deductive program verification.
  • Covers: classical Hoare logic, partial/total correctness, weakest liberal preconditions, examples with Why3 and SMT solvers.
  • Slides
  • Running example in Why3: ISQRT (complete solutions),
  • Canevas for exercises: Exercise 1, Exercise 2, Exercise 3
• Lecture 2 (December 20th): More advanced topics in program verification
  • Covers: blocking semantics, treatment of local variables, ghost variables and labels, function calls and modularity aspects, specification of data types and programs on arrays.
  • Slides
  • Examples and exercices in Why3: Euclid with ghost variables, Euclid with labels, Exercise: Bezout coefficients, Exercise: linear search in an array
• Lecture 3 (January 17th): Handling of data structures
  • Covers: exceptions, termination proofs, specification using abstract functions, sets, maps, and multi-sets; sum types, lists, inductive predicates.
  • Slides
  • Examples in Why3: Solution of exercise Bezout coefficient, Solution of exercise Linear search, Linear search with an exception, Exact square root, with an exception, List reversal,
  • Exercises: McCarthy's 91 function Binary Search Selection sort
• Lecture 4 (January 24th): Aliasing issues
  • Covers: handling of machine integers and floating-point numbers, call by reference, alias control by static typing.
  • Slides
  • Examples in Why3 or C: Solution of exercise McCarthy's 91 function, Solution of exercise Binary search, Solution of exercise Selection Sort, arith.c, bin_search_int32.c, bin_search.c, clock_drift.c, Stack part 1, Stack part 2, Stack part 3 In place linked-list reversal
• Answering questions related to the project (January 31st)

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 (February 7th): Separation Logic Part 1
  • Covers: fundamentals of Separation Logic (heap predicates, triples, derivation rules)
  • Slides of introduction
  • Slides of Part 1
• Lecture 6 (February 14th): Separation Logic Part 2
  • Covers: representation predicates for list and trees, nested mutable data structures.
  • Slides of Part 2
• Lecture 7 (February 21st): Separation Logic Part 3
  • Covers: reasoning about loops, frame during loops, higher-order functions, and specification of objects.
  • Slides of Part 3
• Lecture 8 (February 28th): Separation Logic Part 4
  • Covers: arrays, frame over array cells, data structures with sharing, soundness proof, and characteristic formulae to integrate Separation Logic in Coq.
  • Slides of Part 4