Concurrent separation logic is a development of Hoare logic adapted to deal with pointers and concurrency. Since its inception, it has been enhanced with a treatment of permissions to enable sharing of data between threads, and a treatment of variables as resource alongside heap cells as resource. An introduction to the logic is given with several examples of proofs, culminating in a treatment of Simpson's 4-slot algorithm, an instance of racy non-blocking concurrency. © 2010 Springer-Verlag London.
CITATION STYLE
Bornat, R. (2010). Separation logic and concurrency. In Formal Methods: State of the Art and New Directions (pp. 217–248). Springer London. https://doi.org/10.1007/978-1-84882-736-3_7
Mendeley helps you to discover research relevant for your work.