Concurrent Separation Logic Assertions capture ownerships of resources 1→n Cannot access resource without ownership ● Shared resources are protected by critical regions (CRs) Transfer of ownership at boundary of CRConcurrent Separation Logic • Assertions capture ownerships of resources • Cannot access resource without ownership • Shared resources are protected by critical regions (CRs) • Transfer of ownership at boundary of CR l  n