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

- 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.

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

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

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

Page generated on 2016/9/21