Introduction to the course    (SLFPreface)

Basics of Separation Logic    (SLFBasic)

Heap predicates    (SLFHprop)

Heap entailment    (SLFHimpl)

Reasoning rules    (SLFRules)

Semantics of weakest preconditions    (SLFWPsem)

Weakest precondition generator    (SLFWPgen)

Magic wand    (SLFWand)

Affine Separation Logic    (SLFAffine)

Arrays and records    (SLFStruct)

Assertions, loops, and n-ary functions    (SLFRich)

Overview of the ingredients    (SLFSummary)

a minimal soundness proof    (SLFMinimal)