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

## Organisation

- Location: bĂ˘timent Sophie Germain, room 1002.
- Time: Tuesday, 16:15 to 19:15.
- First course: December 6th.
- 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 on January 3rd (to be confirmed).

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

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 6th): 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

- Lecture 2 (December 13th): 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 3th): Ghost code, More data structures, Exceptions, Computer Arithmetic
- Covers: termination, ghost code, lemma functions, sum types, lists ; handling exceptions ; computer arithmetic : machine integers, floating-point numbers.

- Lecture 4 (January 10th): Aliasing issues
- Covers: call by reference, alias control by static typing ; component-as-array modeling for pointer programs.

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

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

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

- Lecture 7 (January 31st, to be confirmed): Separation Logic 3
- Covers: reasoning about loops, about aliasing, about local state, specification of higher-order functions, in particular iterators, characteristic formulas.

- Lecture 8 (February 7th, to be confirmed): Separation Logic 4
- Covers: higher-order representation predicates, resource analysis, complexity analysis, fractional and read-only permissions, parallelism, lock invariants, ghost variables and state.

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

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