# MPRI Course 2-36-1: Proof of Program

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

The page for year 2017-2018 is here

## Organisation

• Location: bâtiment Sophie Germain, room 2036.
• Time: Wednesday, 16:00 to 19:00.
• First course: December 7th.
• Project description: end of December.
• Project due: February 27th
• Exam: March 1st

## Tools

Example programs for some lectures will be using the verification environment Why3. There is an on-line version of Why3 that can be used to replay the simplest examples. However, for more complex examples and for the project that require several provers, it is necessary to install Why3 and the automated provers.

You may find detailed instructions in this installation procedure.

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

## Exam

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

## Project

The project was provided on January 10th.

The project consists of the formalization of several algorithms for answering range sum queries. Here is the skeleton file provided.

To install Why3 and the automated provers, follow the installation procedure.

## Lectures

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.

• All lectures, for printing:
• Lecture 5 (January 25th): Separation Logic 1
• February 1st, Lab session, help with the project, same room as usual, bring your laptop
• Lecture 6 (February 8th): Separation Logic 2
• Lecture 7 (February 15th): Separation Logic 3
• Covers: reasoning about loops, about aliasing, about local state, specification of higher-order functions, in particular iterators, and presentation of the basics characteristic formulae for conducting Separation Logic in the Coq proof assistant.
• Slides of Part 3 and printable version.
• Lecture 8 (February 22th): Separation Logic 4
• Covers: characteristic formulae (continued), higher-order representation predicates for describing containers that own their elements, and extensions of Separation Logic for parallelism and for amortized complexity analysis.
• Slides of Part 4 and printable version.
• All lectures, for printing: see above.

## Previous exams

You may have a look at the exam of 2014. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2015. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2016. Once you have solved all exercises (and not before!), you may check some of the solutions.

## Past versions

Page generated on 2018/1/9