Introduction to the Course    (Preface)

Basic Proofs in Separation Logic    (Basic)

Representation Predicates    (Repr)

Heap Predicates    (Hprop)

Heap Entailment    (Himpl)

Structural Reasoning Rules    (Triples)

Reasoning Rules for Term Constructs    (Rules)

The Magic Wand and Other Operators    (Wand)

Semantics of Weakest Preconditions    (WPsem)

Weakest Precondition Generator    (WPgen)

Soundness of the Weakest Precondition Generator    (WPsound)

Affine Separation Logic    (Affine)

Reasoning about Arrays    (Arrays)

Reasoning about Records    (Records)

Conclusion and Perspectives    (Postscript)

Bibliography    (Bib)

Appendix - The Full Construction    (LibSepReference)

Appendix - Finite Maps    (LibSepFmap)

Appendix - Program Variables    (LibSepVar)

Appendix - Simplification Tactic for Entailments    (LibSepSimpl)

Appendix - Minimalistic Soundness Proof    (LibSepMinimal)