MPRI Lecture 2-36-1

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.



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.

Part 1: Program verification using Hoare Logic, lectured by François Bobot

Part 2: Separation Logic and representation predicates, lectured by Jean-Marie Madiot

More material on the webpage for Part 2.