Separation logic + superposition calculus = heap theorem prover

Juan Antonio Navarro Pérez, Andrey Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In Mary W. Hall, David A. Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011. pages 556-566, ACM, 2011. [doi]

@inproceedings{PerezR11,
  title = {Separation logic + superposition calculus = heap theorem prover},
  author = {Juan Antonio Navarro Pérez and Andrey Rybalchenko},
  year = {2011},
  doi = {10.1145/1993498.1993563},
  url = {http://doi.acm.org/10.1145/1993498.1993563},
  tags = {logic},
  researchr = {https://researchr.org/publication/PerezR11},
  cites = {0},
  citedby = {0},
  pages = {556-566},
  booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011},
  editor = {Mary W. Hall and David A. Padua},
  publisher = {ACM},
  isbn = {978-1-4503-0663-8},
}