This page presents teaching material for Course 2-36-1 "Proof of Program" of the MPRI 2023-2024.
Organisation
- Location: bâtiment Sophie Germain, room 1004.
- Time: Friday, 08:45 to 11:45.
- First course: December 8th.
- Project description: December 21st
- Project due: February 8th
- Exam: to be announced
Tools
Example programs for some lectures will be using the verification environment Why3. There is an on-line 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 was provided on December 21st.
The project consists of the verification of algorithm for finding optimal strategies in two-player games. A skeleton file is provided in this zip archive.
To install Why3 and the automated provers, follow the installation procedure.
Lectures
Slides and examples will be posted here.
Part 1: Program verification using Hoare Logic, lectured by Claude Marché.
- Lecture 1 (December 8th): 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
- Examples of purely logic goals: propositional logic, first-order logic, equality, integer arithmetic
- Simple basic contracts
- Square root in Why3: ISQRT and its full solution
- Canvas for exercises: Exercise 1, Exercise 2, Exercise 3
- Solution to exercise 1: Inefficient sum
- Lecture 2 (December 15th): 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 or 4 per page
- Solutions to exercices of lecture 1: Euclidean division
- Illustrative examples using Why3: Euclid's algorithm for GCD with labels, Incrementation of a section of an array
- Search in an array : the linear version and its solution,
- Home work:
- McCarthy's 91 function,
- Search in an array : the binary version
- Hoare logic rule and WP formula for `for` loops, to do ``on paper''
- Lecture 3 (December 22th): 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, Binary search, WP rule for ``for'' loops (see the slides), Linear search with a for loop: Canvas and Solution
- Examples in Why3 or C from the slides: Euclid's remainder with ghost code, List reversal: Canvas 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:
- Lecture 4 (January 12th): 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:
- Examples in Why3: Stack part 1, Stack part 2, In place linked-list reversal canvas and complete solution
- Optional home work In-place linked-list concatenation
Part 2: Separation Logic and representation predicates, lectured by Jean-Marie Madiot.
- Lecture 5 (January 19th): Separation Logic 1
- Covers: basic heap predicates, mutable lists, list segments, trees, sharing, specification triples.
- slides, exercise sheet
- Lecture 6 (January 26th): Separation Logic 2
- Covers: frame rule, heap entailment, structural rules, reasoning rules for terms, reasoning about functions.
- slides, exercise sheet
- Lecture 7 (February 2nd): Separation Logic 3
- Covers: reasoning about loops, aliasing, local state, higher-order functions and iterators, higher-order representation predicates, separating implication.
- slides, exercise sheet
- Lecture 8 (February 9th): Separation Logic 4
- Covers: access problem, 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.
- 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)