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

• Location: bâtiment Sophie Germain, room 1003.
• Time: Monday, 16:15 to 19:15.
• First course: December 3th.
• Project description: mid December.
• Project due: February 22th
• Exam: March 4th 2018

Project

The project description is here(v1.1).

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

• Lecture 1 (December 3th): Basics of deductive program verification.
  • Slides
  • Running example in Why3: ISQRT
  • Canvas for exercises: Exercise 1, Exercise 2, Exercise 3
• Lecture 2 (December 10th): More advanced topics in program verification
  • Slides
  • Solutions to exercices of lecture 1 Euclide’s algorithm, Fast exponentiation (hint: increase provers’ time limit to 60 seconds)
  • Examples in Why3: Remainder with ghost variables Euclide with ghost variables Euclide with labels Factorial computed with a while loop
  • Canvas for exercises: Bezout coefficients, McCarthy’s 91 function, search in an array linear version and binary version bezout
• Lecture 3 (December 17th): More data structures, Lemma functions, Exceptions
  • Slides
  • Solutions to exercices of lecture 2: Linear search, Binary search.
  • Examples in Why3 or C from the slides: List reversal, Linear search with an exception, Binary search with an exception, Exact square root, with an exception, arith.c, bin_search_int32.c, bin_search.c, clock_drift.c.
  • Home Work: Bezout exercise continued, McCarthy 91 function continued, Prove Fermat’s little theorem for p=3.
• Lecture 4 (January 7th): Aliasing issues
  • Slides
  • Solutions to exercices of lecture 3: Bezout coefficient, McCarthy 91 function, Lemma functions,
  • Examples in Why3: Stack part 1, Stack part 2, In place linked-list reversal
  • Exercises: In-place linked-list concatenation

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

More material on the webpage for Part 2.

• Lecture 5 (January 14th): Separation Logic 1
• Lecture 6 (January 28th): Separation Logic 2
• Lecture 7 (February 4th): Separation Logic 3
• Lecture 8 (February 11th): Separation Logic 4