MPRI Course 2-36-1: Proof of Program

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


Remark: there will be no course on January 10th.


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


The project consists of the formalization of a convex hull algorithm. Here is the canvas file provided.


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