Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

## Proof of Programs (24h, 3 ECTS)

Teacher in charge: Claude Marché

Teachers for 2018-2019: Claude Marché, 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 (2019-2020 version available soon)

Web pages for 2018-2019 are here and there.

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

### Pre-requisites

Basic knowledge on:

• syntax and semantics of first-order logic,
• formal deduction rules,
• operational semantics of programs.

### Evaluation

Students will evaluated by a practical project and a final exam.

The final grade will be computed as : Max( (1/2 exam + 1/2 project), (3/4 exam + 1/4 project) ).

Universités partenaires
Établissements associés