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

• Concurrent programming

• Concurrent separation logic

• Proving liveness

• Separation logics and OS verification