MPRI

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

Organisation

  • Location: bâtiment Sophie Germain, room 1002.
  • Time: Tuesday, 16:15 to 19:15.
  • First course: December 6th.
  • Project description: January 10th
  • Project due: February 23th
  • Exam: Tuesday, February 28th, 16h15-19h15, room 1002

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.

Project

The project was provided on January 10th.

The project consists of the verification of an algorithm for computing convex hulls. A skeleton file is provided in this zip archive

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 Jean-Marie Madiot.

Past Years

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.

You may have a look at the exam of 2017. 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 2019-2020. 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 2020-2021. 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 2021-2022. Once you have solved all exercises (and not before!), you may check some of the solutions.


Page generated on 2024/2/22