MPRI Course 2-36-1: Proof of Program
This page presents teaching material for Course 2-36-1 "Proof of Program" of the MPRI.
- Location: bâtiment Sophie Germain, room 1009.
- First course: December 13rd.
- Exam: March 14th, 13:15 to 16:15, room 1009
Remark: there will be no course on January 10th.
The text of the exam, and a version including some solutions.
The project consists of the formalization of a convex hull algorithm. Here is the canvas file provided.
Part 1: Program verification using Hoare Logic, lectured by Claude Marché.
- Lecture 1 (December 13th): Basics of deductive program verification.
- Lecture 2 (December 20th): More advanced topics in program verification
- Lecture 3 (January 17th): Handling of data structures
- Covers: exceptions, termination proofs, specification using abstract functions, sets, maps, and multi-sets; sum types, lists, inductive predicates.
- Examples in Why3:
Solution of exercise Bezout coefficient,
Solution of exercise Linear search,
Linear search with an exception,
Exact square root, with an exception,
McCarthy's 91 function
- Lecture 4 (January 24th): Aliasing issues
- Covers: handling of machine integers and floating-point numbers, call by reference, alias control by static typing.
- Examples in Why3 or C:
Solution of exercise McCarthy's 91 function,
Solution of exercise Binary search,
Solution of exercise Selection Sort,
Stack part 1,
Stack part 2,
Stack part 3
In place linked-list reversal
- Answering questions related to the project (January 31st)
Part 2: Separation Logic and representation predicates, lectured by Arthur Charguéraud.
- All lectures, for printing:
- Lecture 5 (February 7th): Separation Logic Part 1
- Lecture 6 (February 14th): Separation Logic Part 2
- Covers: representation predicates for list and trees, nested mutable data structures.
- Slides of Part 2
- Lecture 7 (February 21st): Separation Logic Part 3
- Covers: reasoning about loops, frame during loops, higher-order functions, and specification of objects.
- Slides of Part 3
- Lecture 8 (February 28th): Separation Logic Part 4
- Covers: arrays, frame over array cells, data structures with sharing, soundness proof, and characteristic formulae to integrate Separation Logic in Coq.
- Slides of Part 4
Page generated on 2016/9/21