MPRI

MPRI Course 2-36-1: Proof of Program

• Home
• Organisation
• Tools
• Project
• Lectures
• Past years

This page presents teaching material for MPRI Course 2-36-1 "Proof of Program", 2024-2025.

Organisation

• Location: bâtiment Sophie Germain, room 1004.
• Time: Wednesdays, 08:45 to 11:45.
• First course: December 11th.
• Project description: see below
• Project due: Tuesday, February 11th, 2025 23:00 UTC+1
• Exam: Wednesday March 12, 08:45 to 11:45, room 1004

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

The project consists in verifying operations on union of intervals: Enonce. Aide:

Attention à l'utilisation de prédicat inductif. Les prédicats inductifs sont utiles pour des questions de terminaison et d'induction. Si vous utilisez déjà un type algébrique (e.g. "list") qui a ces propriétés, définissez tous vos prédicats en "predicate" définies structurellement sur un de ces arguments (algébrique). Attention d'autant plus si vous avez des "inductive" qui ne sont pas inductif. NB: Si bound_type_eq est équivalent à =, il vaut mieux utiliser ce dernier dans la logique. NB: la correction n'utilise pas de "inductive"

Lectures

Slides and examples will be posted here.

Part 1: Program verification using Hoare Logic, lectured by François Bobot.

• Lecture 1 (December 11th): 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.
  • Slides: original or 4 per page
  • An Early Program Proof by Alan Turing by F. L. Morris and C. B. Jones
  • Examples of purely logic goals using TryWhy3: propositional(Mlw), first-order logic(Mlw), equality(Mlw), integer arithmetic(Mlw)
  • Simple basic contracts(Mlw)
  • Square root in Why3: ISQRT(Mlw),Solution(Mlw)
  • Canvas for exercises: Exercise 1(Mlw), Exercise 2(Mlw), Exercise 3(Mlw)
• Lecture 2 (December 18th): 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.
  • Slides: original
  • Solutions to exercices of lecture 1: Euclidean division, Fast exponentiation (hint to prove lemmas: increase Alt-Ergo's time limit to 60 seconds)
  • Illustrative examples using Why3:
    • Euclid's algorithm for GCD with labels(Mlw, Sol)
    • array incrementation(Mlw)
  • Homeworks:
    • McCarthy 91 function(Mlw)
    • linear search(Mlw)
    • binary search(Mlw)
• Lecture 3 (January 8th): More data structures, Exceptions, Computer Arithmetic
  • Covers: sum types, lists ; handling exceptions ; computer arithmetic : machine integers, floating-point numbers.
  • Slides: original or 4 per page
  • Solutions to home work from lecture 2: McCarthy 91 function(Mlw), Linear search(Mlw), Binary search(Mlw), WP rule for ``for'' loops (see the slides), Linear search with a for loop: Canvas(Mlw) and Solution
  • Examples in Why3 or C from the slides: Euclid's remainder with ghost code(Mlw), List reversal: with ghost code(Mlw) and Solution, Exact square root, with an exception, Linear search with an exception: canvas and solution, Examples of overflow and rounding errors Binary search on 32-bits ints in Why3, Binary search in C, "Clock drift", bounding rounding errors on successive additions of 0.1 ,
  • Home Work:
    • Bézout coefficients (Mlw) using ghost code
    • Lemmas on power function, using lemma functions(Mlw)
    • Prove Fermat's little theorem for p=3 (Mlw)
    • Binary search with an exception(Mlw)
• Lecture 4 (January 15th): Aliasing issues
  • Covers: call by reference, alias control by static typing ; framing issue ; component-as-array modeling for pointer programs.
  • Slides: original or 4 per page
  • Solutions to exercices of lecture 3:
    • Bézout coefficients (Mlw) using ghost code
    • "(Mlw)little Fermat's theorem for n=3 >,
    • "(Mlw)Lemmas on power function, using lemma functions >
    • Binary search with an exception (Mlw)
    • Binary search using machine integers (Mlw)
  • Examples in Why3: " Stack part 1 (Mlw), " Stack part 2 (Mlw), In place linked-list reversal " canvas (Mlw) and " complete solution (Mlw)
  • Optional home work " In-place linked-list concatenation (Mlw)
• January 22th : Lab session for any who need help for the project

Part 2: Separation Logic and representation predicates, lectured by Jean-Marie Madiot.

• Lecture 5 (January 29th): Separation Logic 1
  • Covers: basic heap predicates, mutable lists, list segments, trees, sharing, specification triples.
  • slides, exercise sheet
• Lecture 6 (February 5th): Separation Logic 2
  • Covers: frame rule, heap entailment, structural rules, reasoning rules for terms, reasoning about functions.
  • slides, exercise sheet
• Lecture 7 (February 12th): Separation Logic 3
  • Covers: reasoning about loops, aliasing, local state, higher-order functions and iterators, higher-order representation predicates, separating implication, access problem.
  • slides, exercise sheet
• Lecture 8 (February 19th): 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.
  • slides, exercise sheet

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 this year's exam. Once you have solved all exercises (and not before!), you may check some of the solutions.

• Course given in 2023-2024 (similar content)
• Course given in 2022-2023 (similar content)
• Course given in 2021-2022 (similar content)
• Course given in 2020-2021 (similar content)
• Course given in 2019-2020 (similar content)
• Course given in 2018-2019 (similar content)
• Course given in 2017-2018 (similar content)
• Course given in 2016-2017 (similar content)
• Course given in 2015-2016 (similar content)
• Course given in 2014-2015 (similar content)
• Course given in 2013-2014 (similar content)
• Course given in 2012-2013 (different content)
• Course given in 2011-2012 (different content)