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 2017-2018: 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.

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