MPRI Course 2-36-1: Proof of Program
This page presents teaching material for Course 2-36-1 "Proof of Program" of the MPRI 2015-2016.
- Location: bâtiment Sophie Germain, room 2035.
- Time: Thursday, 8:45 to 11:45.
- First course: December 10th.
- Project description: end of December.
- Project due: February 15th, at 10pm (21:00 UTC).
- Exam: March 3rd.
The text of the exam, and a version including the solutions.
The project was provided on December 18th.
The project consists of the formalization of a divide-and-conquer algorithm to solve the closest pair problem. Here is the skeleton file provided.
Slides and examples will be posted here.
Part 1: Program verification using Hoare Logic, lectured by Claude Marché.
- Lecture 1 (December 10th): Basics of deductive program verification.
- Covers: classical Hoare logic, partial correctness, weakest liberal preconditions, blocking semantics, simple examples with Why3 and SMT solvers.
- Running example in Why3: ISQRT
- Canvas for exercises: Exercise 1, Exercise 2, Exercise 3
- Lecture 2 (December 17th): More advanced topics in program verification
- Covers: treatment of local variables, ghost variables and labels, function calls and modularity aspects, termination, specification languages, axiomatic specifications, programs on arrays.
- Solutions to exercices of lecture 1: Euclide's algorithm, Fast exponentiation (hint: increase provers' time limit to 60 seconds
- Examples in Why3:
Euclide with ghost variables,
Euclide with labels,
Factorial computed with a while loop,
- Home work:
McCarthy's 91 function,
Search in an array, linear version
- Lecture 3 (January 7th): More data structures, Lemma functions, Exceptions
- Covers: lemma functions ; products and sum types, lists ; exceptions ; computer arithmetic.
- Solutions to exercices of lecture 2:
- Examples in Why3 or C from the slides:
Linear search with an exception,
Binary search with an exception,
Exact square root, with an exception,
- Home Work: Bezout exercise continued,
McCarthy 91 function continued,
Prove Fermat's little theorem for p=3
- Lecture 4 (January 14th): Aliasing issues
- No lecture on January 21th
Part 2: Separation Logic and representation predicates, lectured by Arthur Charguéraud.
- Lecture 5 (January 28th): Separation Logic 1
- Lecture 6 (February 4th): Separation Logic 2
- February 11th, Lab session from *9h30* to 12h: help with the project, same room as usual, bring your laptop
- Lecture 7 (February 18th): Separation Logic 3
- Covers: specification of higher-order functions, higher-order representation predicates for specifying advanced data structures, and ownership transfer.
- Slides of Part 3
and printable version.
- Lecture 8 (February 25th): Separation Logic 4
- Covers: higher-order representation predicates: arrays and iterations; Separation Logic in the Coq proof assistant; extensions of Separation Logic for parallelism and concurrency.
- Slides of Part 4
and printable version.
Page generated on 2016/9/21