MPRI

- Proof of Programs (24h, 3 ECTS)

Proof of Programs (24h, 3 ECTS)

Teacher in charge: Jean-Marie Madiot (anc., Claude Marché)

Teachers for 2024-2025: François Bobot, Jean-Marie Madiot

Lessons will be given in French by default, in English upon request. The slides and the lecture notes will be in English. In the past 3 years, the course has been taught in English.

Dates and files associated with the course are posted on the webpage of the course http://www.lri.fr/~marche/MPRI-2-36-1/

Objectives of the Course

Introduction to the various concepts and formalisms towards the proof that a program respects a given formal specification.

Outline

Basics of deductive program verification:
- classical Hoare logic, partial/total correctness, weakest liberal preconditions, examples with Why3 and SMT solvers.
More advanced topics in program verification:
- treatment of local variables, effects, exceptions, blocking semantics, modularity aspects.
Handling of data structures:
- specification using abstract functions, sets, maps, and multi-sets; program on arrays; handling of machine integers and floating-point numbers.
Aliasing issues:
- call by reference, alias control by static typing.
Separation Logic Part 1:
- basic heap predicates, mutable lists and trees, specification triples, list segments, frame rule.
Separation Logic Part 2:
- trees with invariants, arrays, structures with sharing, heap entailment, interpretation of triples, reasoning rules.
Separation Logic Part 3:
- specification of higher-order functions, higher-order representation predicates for specifying advanced data structures, and ownership transfer.
Separation Logic Part 4:
- higher-order representation predicates: arrays and iterations; Separation Logic in the Coq proof assistant; extensions of Separation Logic for parallelism and concurrency.