MPRI Lecture 2-36-1

This page presents teaching material for Part 1 of Course 2-36-1 “Proof of Program” of the MPRI 2018-2019. For the second part, see the webpage for Part 2.

Organisation

Project

The project description is here(v1).

You will need why3 version 1.1.0

Pratical lab: January 21th and maybe February 18th

An important point is that you are required to realize the project using the Why3 environment for program verification. We built a special page dedicated to the installation procedure of Why3 here.

We recommend that you install Why3, and theorem provers, as indicated, as soon as possible. The lectures will be partly illustrated by examples using Why3, so having a working Why3 environment on your computer will allow you to replay the examples of the lectures, and improve your Why3 skills as soon as possible.

In order to install CVC4 you should use the binary distribution. After the download put the binary in your path (in /usr/local/bin for example), with a name like cvc4-1.6. Don’t forget to make the binary executable.

The exact executable used for the correction are: Alt-Ergo 2.0.0 (through opam), Eprover 1.9.1-001, Z3 4.4.1, CVC4 1.5. You can use other provers and version recognized by why3 for the project.

Lectures

Slides and examples will be posted here.

Part 1: Program verification using Hoare Logic, lectured by François Bobot

Part 2: Separation Logic and representation predicates, lectured by Jean-Marie Madiot

More material on the webpage for Part 2.