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 Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA