title:
Proofs of Programs
Preuves de programmes
manager:
Jean-Marie Madiot
ects:
3
period:
2
hours:
24
weeks:
8
hours-per-week:
3
language:
English on request
lang:
track:
B
themes:
Logic/Proof, Semantic/Languages, Verification
order:
2.36.1
successor:
progproofs
link:
view
  • [2.36.1]
  • Proofs of Programs
    Preuves de programmes
  • Language:
  • Period:
  • 2.
  • Duration:
  • 24h (3h/week).
  • ECTS:
  • 3.
  • Manager:
  • Jean-Marie Madiot.

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 4 years, the course has been taught in English.

Dates and files associated with the course are posted on the webpage of the course https://marche.gitlabpages.inria.fr/lecture-deductive-verif/

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( (2/3 exam + 1/3 project), (3/4 exam + 1/4 project) ).