. Dafny, An Automatic Program Verifier for Functional Correctness, p.16, 2010.

M. Barnett, B. E. Chang, R. Deline, B. Jacobs, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, p.FMCO, 2006.
DOI : 10.1007/11804192_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.2596

M. Barnett, . Leino, and W. Schulte, The Spec# Programming System, 2005.
DOI : 10.1007/978-3-540-30569-9_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.2133

J. Berdine, C. Calcagno, and P. W. O-'hearn, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, p.FMCO, 2005.
DOI : 10.1007/11804192_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.63.613

J. Berdine, C. Calcagno, and P. W. O-'hearn, Symbolic Execution with Separation Logic, p.APLAS, 2005.
DOI : 10.1007/11575467_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.107.2776

J. Brotherston, R. Bornat, and C. Calcagno, Cyclic proofs of program termination in separation logic, p.POPL, 2008.

C. Calcagno, D. Distefano, P. O-'hearn, and H. Yang, Compositional shape analysis by means of bi-abduction, p.POPL, 2009.

C. Calcagno, M. Parkinson, and V. Vafeiadis, Modular Safety Checking for Fine-Grained Concurrency, In SAS. LNCS, 2007.
DOI : 10.1007/978-3-540-74061-2_15
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.4528

B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi, Proving that programs eventually do something good, p.7, 2007.
DOI : 10.1145/1190216.1190257
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.7543

D. Distefano, P. W. O-'hearn, and H. Yang, A Local Shape Analysis Based on Separation Logic, In: In TACAS, vol.24, issue.3, 2006.
DOI : 10.1145/514188.514190
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.222.9915

D. Distefano and M. J. Parkinson, jStar: towards practical verification for Java, p.OOPSLA, 2008.

A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv, Local Reasoning for Storable Locks and Threads, p.APLAS, 2007.
DOI : 10.1007/978-3-540-76637-7_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.6546

D. Harel, D. Kozen, and J. Tiuryn, Dynamic logic, 1984.

B. Jacobs, J. Smans, and F. Piessens, A Quick Tour of the VeriFast Program Verifier, p.APLAS, 2010.
DOI : 10.1007/978-3-642-17164-2_21

K. Leino and P. Rümmer, A Polymorphic Intermediate Verification Language: Design and Logical Encoding, p.TACAS, 2010.
DOI : 10.1007/978-3-642-12002-2_26
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.149.9780

K. R. Leino and P. Müller, A Basis for Verifying Multi-threaded Programs, p.ESOP, 2009.
DOI : 10.1007/BF01211617
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.146.3600

M. J. Parkinson and G. M. Bierman, Separation logic and abstraction, p.POPL, 2005.
DOI : 10.1145/1040305.1040326
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.5332

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, p.LICS, 2002.
DOI : 10.1109/LICS.2002.1029817
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.5322

G. Rosu, C. Ellison, and W. Schulte, Matching Logic: An Alternative to Hoare/Floyd Logic, p.AMAST, 2010.

J. Smans, B. Jacobs, and F. Piessens, Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic, p.2009, 2009.
DOI : 10.1007/978-3-642-00590-9_27

H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook et al., Scalable Shape Analysis for Systems Code, p.CAV, 2008.
DOI : 10.1007/978-3-540-70545-1_36
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.143.9907