This page presents teaching material for Part 1 of Course 2-36-1 "Proof of Program" of the MPRI 2017-2018. For the second part, see the webpage for Part 2.

- Location: bâtiment Sophie Germain, room 1012.
- Time: Wednesday, 12:45 to 15:45.
- First course: December 6th.
- Project description: end of December.
- Project due: February 25th.
- Exam: March 7th 2018 (exam, solution).

The project is described here and the file to fill in is topo.mlw.

You will need why3 version 0.87.3

Pratical lab: January 17th and maybe February 21th

An important point is that you are required to realize a project using the Why3 environment for program verification. We built a special page dedicated to the installation procedure of Why3 here.

We recommend that you install Why3, and theorem provers, as indicated, as soon as possible. The lectures will be partly illustrated by examples using Why3, so having a working Why3 environment on your computer will allow you to replay the examples of the lectures, and improve your Why3 skills as soon as possible.

Slides and examples will be posted here.

- Lecture 1 (December 6th): Basics of deductive program verification.
- Slides
- Running example in Why3: ISQRT
- Canvas for exercises: Exercise 1, Exercise 2, Exercise 3

- Lecture 2 (December 13th): More advanced topics in program verification
- Slides
- Solutions to exercices of lecture 1 Euclide's algorithm, Fast exponentiation (hint: increase provers' time limit to 60 seconds)
- Examples in Why3: Remainder with ghost variables Euclide with ghost variables Euclide with labels Factorial computed with a while loop
- Canvas for exercises: Bezout coefficients, McCarthy's 91 function, search in an array linear version and binary version

- Lecture 3 (December 20th): More data structures, Lemma functions, Exceptions
- 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 17th): Aliasing issues
- 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

More material on the webpage for Part 2.

- Lecture 5 (January 24th): Separation Logic 1
- Lecture 6 (January 31th): Separation Logic 2
- Lecture 7 (February 7th): Separation Logic 3
- Lecture 8 (February 14th): Separation Logic 4