Shape analysis bibliography
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