PLClub Discussion Group

Concurrent Separation Logic and Subjective Auxiliary State

This week I’ll first introduce concurrent separation logic, and then subjective auxiliary state, a technique that allows for compositional reasoning when using auxiliary (or ghost) state.

This topic is (sequentially) composed of two talks: we will continue next week where Irene will talk about follow-up work for reasoning about fine-grained concurrency.