This page presents teaching material for MPRI Course "Proofs of Programs" (Acronym: PROGPROOFS, was formerly MPRI 2-36-1), 2025-2026.
Organisation
- Location: bâtiment Sophie Germain, room 1006 (double check the room on the timetable).
- Time: Tuesdays, 16:15 to 19:15
- First course: December 9, 2025
- Exam: Tuesday, March 10, 2026
- Teachers: Andrei Paskevich then Jean-Marie Madiot
Tools
Example programs for some lectures will be using the verification environment Why3. There is an online version of Why3 that can be used to replay the simplest examples. However, for more complex examples and for the project that require several provers, it is necessary to install Why3 and the automated provers.
You may find detailed instructions in this installation procedure.
Project
There will be a project for part 1 of the course.
Lectures
Slides and examples will be posted here.
Part 1: Program verification using Hoare Logic, lectured by Andrei Paskevich.
- Lecture 1 (December 9): Basics of deductive program
verification.
- Covers: background on automated deduction, classical Hoare logic, partial correctness, weakest liberal preconditions, simple examples with Why3 and SMT solvers. More modern approach with a ML-style language, blocking semantics.
- Lecture 2 (December 16): More advanced topics in program verification
- Covers: treatment of local variables, labels, function calls and modularity aspects, termination, specification languages, axiomatic specifications, product types programs on arrays.
- Lecture 3 (January 6): More data structures, Exceptions, Computer Arithmetic
- Covers: sum types, lists ; handling exceptions ; computer arithmetic : machine integers, floating-point numbers.
- No lecture January 13
- Lecture 4 (January 20): Aliasing issues
- Covers: call by reference, alias control by static typing ; framing issue ; component-as-array modeling for pointer programs.
- January 27 : Lab session for any who need help for the project
Part 2: Separation Logic, lectured by Jean-Marie Madiot.
- Lecture 5 (February 3): Separation Logic 1
- Covers: basic heap predicates, mutable lists, list segments, trees, sharing, specification triples, frame rule.
- slides, exercise sheet
- Lecture 6 (February 10): Separation Logic 2
- Covers: heap entailment, structural rules, reasoning rules for terms, functions, loops, higher-order functions and iterators
- slides, exercise sheet, Rocq files: lists.v, trees.v
- Lecture 7 (February 17): Separation Logic 3
- Covers: iteration and higher-order representation predicates, separating implication, parallelism and concurrency, locks invariants, fractional permissions, ghost state.
- slides, exercise sheet, Rocq files: iter.v, listof.v
- Lecture 8 (February 24): Separation Logic 4
- Covers: ghost state, resource algebras, later modality, invariants, persistent predicates, weakest preconditions, Iris, resource analysis, complexity analysis.
- slides, exercise sheet, Rocq files: ra_SF.v, ra_H.v, mon_counter.v