A Formal C Memory Model for Separation Logic

Robbert Krebbers. A Formal C Memory Model for Separation Logic. Journal of Automated Reasoning, 57(4):319-387, 2016. [doi]

@article{Krebbers16,
  title = {A Formal C Memory Model for Separation Logic},
  author = {Robbert Krebbers},
  year = {2016},
  doi = {10.1007/s10817-016-9369-1},
  url = {http://dx.doi.org/10.1007/s10817-016-9369-1},
  researchr = {https://researchr.org/publication/Krebbers16},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {57},
  number = {4},
  pages = {319-387},
}