In recent years, separation logic has brought great advances in the world of verification. However, there is a disturbing trend for each new library or concurrency primitive to require a new separation logic. I will argue that we shouldn't be inventing new separation logics, but should find the right logic to reason about interference, and have a powerful abstraction mechanism to enable the library's implementation details to be correctly abstracted. Adding new concurrency libraries should simply be a matter of verification, not of new logics or metatheory. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Parkinson, M. (2010). The next 700 separation logics (invited paper). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6217 LNCS, pp. 169–182). https://doi.org/10.1007/978-3-642-15057-9_12
Mendeley helps you to discover research relevant for your work.