@article{abstraction-refinement,
  author = {Gardner, Philippa and Raad, Azalea and Wheelhouse, Mark J. and Wright, Adam},
  title = {{Abstract Local Reasoning for Concurrent Libraries: Mind the Gap}},
  journal = {Proceedings of the 30\textsuperscript{th} Conference on the Mathematical Foundations of Programming Semantics ({MFPS'14})},
  year = {2014},
  volume = {308},
  pages = {147--166},
  abstract = {We study abstract local reasoning for concurrent libraries. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.},
  doi = {10.1016/j.entcs.2014.10.009}
}