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

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

Note that there will be no questions on characteristic formulae.

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

The project was provided on December 18th.

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

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

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.

Page generated on 2016/9/21