- Location: bâtiment Sophie Germain, room 2035.
- Time: Thursday, 8:45 to 11:45.
- First course: December 10th.
- Project description: end of December.
- Project due: February 15th, at 10pm (21:00 UTC).
- Exam: March 3rd.

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

- Location: bâtiment Sophie Germain, room 2035.
- Time: Thursday, 8:45 to 11:45.
- First course: December 10th.
- Project description: end of December.
- Project due: February 15th, at 10pm (21:00 UTC).
- Exam: March 3rd.

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

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.

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.

Page generated on 2016/9/21