Lectures at the ENS Lyon Winter School on Separation Logics and Applications (2011)