Theorem Proving and Provers (TPP2016) http://pllab.is.ocha.ac.jp/~asai/tpp2016/ J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures* Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, held July 22-25, 2002 in Copenhagen, Denmark. http://www.cs.cmu.edu/~jcr/seplogic.pdf