MPRI Course 2-36-1: Proof of Program

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

Organisation

Exam

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

Project

The project was provided on December 18th.

The project consists of the formalization of a divide-and-conquer algorithm to solve the closest pair problem. Here is the skeleton file provided.

Lectures

Slides and examples will be posted here.

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

• Lecture 1 (December 10th): Basics of deductive program verification.
  • Covers: classical Hoare logic, partial correctness, weakest liberal preconditions, blocking semantics, simple examples with Why3 and SMT solvers.
  • Slides
  • Running example in Why3: ISQRT
  • Canvas for exercises: Exercise 1, Exercise 2, Exercise 3
• Lecture 2 (December 17th): More advanced topics in program verification
  • Covers: treatment of local variables, ghost variables and labels, function calls and modularity aspects, termination, specification languages, axiomatic specifications, programs on arrays.
  • Slides
  • Solutions to exercices of lecture 1: Euclide's algorithm, Fast exponentiation (hint: increase provers' time limit to 60 seconds
  • Examples in Why3: Euclide with ghost variables, Euclide with labels, Factorial computed with a while loop,
  • Home work: Bezout coefficients, McCarthy's 91 function, Search in an array, linear version binary version
• Lecture 3 (January 7th): More data structures, Lemma functions, Exceptions
  • Covers: lemma functions ; products and sum types, lists ; exceptions ; computer arithmetic.
  • Slides
  • Solutions to exercices of lecture 2: Linear search, Binary search,
  • Examples in Why3 or C from the slides: Lemma functions List reversal, Linear search with an exception, Binary search with an exception, Exact square root, with an exception, arith.c, bin_search_int32.c, bin_search.c, clock_drift.c,
  • Home Work: Bezout exercise continued, McCarthy 91 function continued, Prove Fermat's little theorem for p=3
• Lecture 4 (January 14th): Aliasing issues
  • Covers: call by reference, alias control by static typing ; component-as-array modeling for pointer programs.
  • Slides
  • Solutions to exercices of lecture 3: Bezout coefficient, McCarthy 91 function, Lemma functions,
  • Examples in Why3: Stack part 1, Stack part 2, In place linked-list reversal
  • Exercises: In-place linked-list concatenation
• No lecture on January 21th

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

• Lecture 5 (January 28th): Separation Logic 1
  • Covers: heap predicates, mutable lists and trees, specification triples, list segments, frame rule.
  • Slides of introduction
  • Slides of Part 1 and printable version.
• Lecture 6 (February 4th): Separation Logic 2
  • Covers: trees with invariants, arrays, structures with sharing, heap entailment, interpretation of triples, reasoning rules.
  • Slides of Part 2 and printable version.
• February 11th, Lab session from *9h30* to 12h: help with the project, same room as usual, bring your laptop
• Lecture 7 (February 18th): Separation Logic 3
  • Covers: specification of higher-order functions, higher-order representation predicates for specifying advanced data structures, and ownership transfer.
  • Slides of Part 3 and printable version.
• Lecture 8 (February 25th): Separation Logic 4
  • Covers: higher-order representation predicates: arrays and iterations; Separation Logic in the Coq proof assistant; extensions of Separation Logic for parallelism and concurrency.
  • Slides of Part 4 and printable version.