Navarro Pérez, JA; Rybalchenko, A; (2011) Separation logic + superposition calculus = heap theorem prover. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). (pp. 556 - 566).