I. Foundations:

* The Logic of Bunched Implications.

P.W. O'Hearn and D. J. Pym.  Bulletin of Symbolic Logic, 5(2), June 1999, pp215-244

* Intuitionistic Reasoning about Shared Mutable Data Structure.

John Reynolds. Millennial Perspectives in Computer Science. 2000

* BI as an Assertion Language for Mutable Data Structures.

Samin Ishtiaq, Peter O'Hearn. POPL'01

* Separation Logic: A Logic for Shared Mutable Data Structures.

John Reynolds. LICS'02

II. Separation Logic-based Analyses

* Local Reasoning about Programs that Alter Data Structures.

 Peter W. O'Hearn, John C. Reynolds, Hongseok Yang. CSL 2001

* Symbolic Execution with Separation Logic.

 Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn. APLAS 2005

* A Local Shape Analysis Based on Separation Logic.

Dino Distefano, Peter W. O'Hearn, Hongseok Yang. TACAS 2006

* Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic.

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang. SAS 2006

* Automatic Termination Proofs for Programs with Shape-Shifting Heaps.

Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn. CAV 2006

* Interprocedural Shape Analysis with Separated Heap Abstractions.

Alexey Gotsman, Josh Berdine, Byron Cook. SAS 2006

* Types, bytes, and separation logic.

Harvey Tuch, Gerwin Klein, Michael Norrish. POPL 2007.

* Shape Analysis with Inductive Recursion Synthesis.

Bolei Guo, Neil Vachharajani, David I. August. PLDI 2007

* Footprint Analysis: A Shape Analysis that Discovers Preconditions.

C Calcagno, D Distefano, PW O'Hearn and H Yang. SAS 2007

* Shape analysis for composite data structures.

J Berdine, C Calcagno, B Cook, D Distefano, PW O'Hearn, T Wies and H Yang. CAV 2007

* Local Action and Abstract Separation Logic.

C Calcagno, PW O'Hearn and H Yang. LICS'07