MPRI Course 2-36-1: Proof of Program
This page presents teaching material for Course 2-36-1 "Proof of Program" of the MPRI 2014-2015.
Organisation
- Location: bâtiment Sophie Germain, room 1009.
- Time: Thursday, 16:15 to 19:15.
- First course: December 11th.
- Project due: Extended dead-line: February 23th at 19:00 UTC+1.
- Exam: March 12th, 16:15 to 19:15.
Remark: there will be no course on January 8th and March 5th.
Exam
Note that there will be no questions on characteristic formulae.
The text of the exam, and a version including some solutions.
Project
The project was provided on December 18th.
It will consist of a formal development using Why3 and automated provers.
The project consists of the formalization of two-player games. Here is the canvas file provided.
Lectures
Slides and examples will be posted here.
[Warning: dates to be confirmed.]
Part 1: Program verification using Hoare Logic, lectured by Claude Marché.
- Lecture 1 (December 11th): Basics of deductive program verification.
- Covers: classical Hoare logic, partial/total correctness, weakest liberal preconditions, blocking semantics, examples with Why3 and SMT solvers.
- Slides
- Running example in Why3: ISQRT
- Canvas for exercises: Exercise 1, Exercise 2, Exercise 3
- Lecture 2 (December 18th): More advanced topics in program verification
- Covers: blocking semantics continued, treatment of local variables, ghost variables and labels, function calls and modularity aspects, termination, specification languages, lemma functions.
- Slides
- Solutions to exercices of lecture 1: Euclide's algorithm, Fast exponentiation
- Examples in Why3:
Euclide with ghost variables,
Euclide with labels,
- Exercises:
Bezout coefficients,
McCarthy's 91 function
Lemma functions
- Lecture 3 (January 15th): Handling of data structures
- Covers: products and sum types, lists ; specification using abstract types, sets, maps, arrays; exceptions ; computer arithmetic.
- Slides
- Solutions to exercices of lecture 2:
Bezout coefficient,
McCarthy 91 function,
Lemma functions,
- Examples in Why3 or C:
List reversal,
Linear search,
Linear search with an exception,
Exact square root, with an exception,
arith.c,
bin_search_int32.c,
bin_search.c,
clock_drift.c,
- Exercises:
Binary Search
- Lecture 4 (January 22th): Aliasing issues
- Answering questions related to the project (one week in February)
Part 2: Separation Logic and representation predicates, lectured by Arthur Charguéraud.
- All lectures, for printing:
- Lecture 5 (January 29th): Separation Logic 1
- Lecture 6 (February 5th): Separation Logic 2
- Lab session (February 12th): help on the project
- Lecture 7 (February 19th): Separation Logic 3
- Covers: loops, soundness theorem, higher-order functions, deallocation, concurrency
- Slides of Part 3
and printable version
- Exercises and solutions to proofs are provided at the end of the slides.
- Lecture 8 (February 26th): Separation Logic 4
- Covers: arrays, polymorphic representation predicates, recursive ownership, characteristic formulae
- Slides of Part 4
and printable version
- Exercises and solutions to proofs are provided at the end of the slides.
- All lectures, for printing: see above.
Page generated on 2016/9/21