Separation logic + superposition calculus = heap theorem prover.

Juan Antonio Navarro Prez, Andrey Rybalchenko

Browse the full PLDI paper archive.