MPRI Course 2-36-1: Proof of Program

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


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

Part 2: Separation Logic and representation predicates, lectured by Arthur Charguéraud.

Page generated on 2016/9/21