This page presents teaching material for Course 2-36-1 "Proof of Program" of the MPRI 2020-2021.

## Organisation

- Location: video-conference, link to be announced
- Time: Wednesday, 08:45 to 11:45.
- First course: December 9th.
- Project description: to be announced
- Project due: to be announced
- 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 will be provided in December.

It will consist of the formal verification of an algorithm, using Why3 and automated provers.

## Lectures

Slides and examples will be posted here.

**Part 1**: Program verification using Hoare Logic, lectured by Claude MarchĂ©.

- Lecture 1 (December 9th): 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.
- 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 16th): More advanced topics in program verification
- Covers: a ML-style language, blocking semantics, treatment of local variables, labels, function calls and modularity aspects, termination, specification languages, axiomatic specifications, product types, ghost code, lemma functions, programs on arrays.
- Slides: original or 4 per page
- 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: Euclide's algorithm for GCD with labels, Euclide's remainder without ghost code and then with ghost code, A Lemma function
- Home work:
- McCarthy's 91 function,
- Bézout coefficients,
- Factorial computed with a while loop,
- Search in an array : the linear version and then the binary version
- Prove Fermat's little theorem for p=3
- Hoare logic rule and WP formula for `for` loops, to do ``on paper''

- Lecture 3 (January 6th): 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: Bezout coefficient, Factorial function, Lemmas on power function, using lemma functions, Linear search, 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: 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 in C, "Clock drift", bounding rounding errors on successive additions of 0.1 ,
- Home Work: (still to complete) McCarthy 91 function (still to do) little Fermat's theorem for n=3, Binary search with an exception,

- Lecture 4 (January 13th): Aliasing issues
- Covers: call by reference, alias control by static typing ; component-as-array modeling for pointer programs.
- Slides: original or 4 per page
- Solutions to exercices of lecture 3: McCarthy's 91 function Binary search with an exception
- Examples in Why3: Stack part 1, Stack part 2, In place linked-list reversal canvas and complete solution
- Home work In-place linked-list concatenation

**Part 2**: Separation Logic and representation predicates, lectured by Jean-Marie Madiot. Ask Jean-Marie by email or in person if you'd like printable versions. Please note that the slides are subject to occasional change.

- Lecture 5 (January 20th): Separation Logic 1
- Covers: basic heap predicates, mutable lists, list segments, trees, sharing, specification triples.

- Lecture 6 (January 27th): Separation Logic 2
- Covers: frame rule, heap entailment, structural rules, reasoning rules for terms, reasoning about functions.

- Lecture 7 (February 3rd): Separation Logic 3
- Covers: reasoning about loops, about aliasing, about local state, specification of higher-order functions, in particular iterators, and presentation of the basics characteristic formulae for conducting Separation Logic in the Coq proof assistant.

- Lecture 8 (February 10th): Separation Logic 4
- Covers: characteristic formulae (continued), higher-order representation predicates for describing containers that own their elements, and extensions of Separation Logic for parallelism and for amortized complexity analysis.

## 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.

- 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)