Introduction to the Course    (Preface)

Basic Proofs in Separation Logic    (Basic)

Representation Predicates    (Repr)

Heap Predicates    (Hprop)

Heap Entailment    (Himpl)

Reasoning Rules    (Rules)

Semantics of Weakest Preconditions    (WPsem)

Weakest Precondition Generator    (WPgen)

The Magic Wand Operator    (Wand)

Affine Separation Logic    (Affine)

Arrays and Records    (Struct)

Assertions, Loops, N-ary Functions    (Rich)

Triples for Nondeterministic Languages    (Nondet)

Triples for Partial Correctness    (Partial)

Conclusion and Perspectives    (Postscript)

Bibliography    (Bib)

Appendix - The Full Construction    (LibSepReference)

Appendix - Finite Maps    (LibSepFmap)

Appendix - Program Variables    (LibSepVar)

Appendix - Simplification of Entailments    (LibSepSimpl)

Appendix - Minimalistic Soundness Proof    (LibSepMinimal)