Resources, concurrency, and local reasoning

In this paper we show how a resource-oriented logic, separation logic, can be used to reason about the usage of resources in concurrent programs.