5. Week 05: Verifying Concurrent Programs

5.1. Mandatory Reading

• Shared-memory concurrency: Concurrent Separation Logic (slides by Xavier Leroy)

5.2. Accompanying Code

• Concurrent Separation Logic in Coq

5.3. Recommended Reading

• Maurice Herlihy and Nir Shavit: The Art of Multiprocessor Programming, 2008
• Stephen Brookes and Peter W. O’Hearn: Concurrent Separation Logic, 2016
• Viktor Vafeiadis: Concurrent Separation Logic and Operational Semantics, 2011