MPRI Course: Proofs of Programs

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 1002.
Time: Tuesdays, 16:15 to 19:15
First course: December 9, 2025
Exam: Tuesday, March 3 or 10, 2025
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 and representation predicates, lectured by Jean-Marie Madiot.

Lecture 5 (February 3): Separation Logic 1
- Covers: basic heap predicates, mutable lists, list segments, trees, sharing, specification triples.
Lecture 6 (February 10): Separation Logic 2
- Covers: frame rule, heap entailment, structural rules, reasoning rules for terms, reasoning about functions.
Lecture 7 (February 17): Separation Logic 3
- Covers: reasoning about loops, aliasing, local state, higher-order functions and iterators, higher-order representation predicates, separating implication, access problem.
Lecture 8 (February 24): Separation Logic 4
- Covers: iteration with higher-order representation predicates, resource analysis, complexity analysis, fractional permissions, parallelism, concurrency, lock invariants, ghost variables, ghost state, modalities.

Past Years

You may have a look at the exam of 2014. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2015. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2016. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2017. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2019-2020. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2020-2021. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2021-2022. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2022-2023. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at the exam of 2023-2024. Once you have solved all exercises (and not before!), you may check some of the solutions.

You may have a look at last year's exam. Once you have solved all exercises (and not before!), you may check some of the solutions.