MPRI Course 2-36-1: Proof of Program

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



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

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

Page generated on 2016/9/21