Separation Logic Course

I teach at the MPRI (Parisian Master of Research in Computer Sciences), the program verification course, together with Claude Marché.

I cover the following chapters.

  • Heap predicates, heap entailment, interpretation triples, derivation rules.
  • Representation predicates for list and trees, nested mutable data structures, ownership transfer.
  • Reasoning about loops, frame during loops, higher-order functions, iterators.
  • Arrays, records and objects, frame over individual cells, data structures with sharing.
  • Extensions of Separation Logic for read-only permissions, parallelism, concurrency, and amortized analysis.
  • Characteristic formulae for integrating Separation Logic in Coq.

Slides from Febuary 2017:

Additional information may be found on the page of the page of the course.