• Contents of the course available from the Software Foundations website.
  
  
• Solutions to exercises are available. Make sure to try hard before requesting hints.
  
  
• The companion course notes, formatted using LaTeX, cover most of the contents.
  
  
• More advanced material is covered in my habilitation manuscript.
  
  

• 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.

Here are the slides from Febuary 2017:

• Slides of the 4 courses
• Version for printing (4 slides per page)