1. E. Abrahám, F. S. De-boer, W. De-roever, and M. Steffen, Tool-supported proof system for multithreaded Java, G. Andrews. Concurrent Programming: Principles and Practice. Benjamin/Cummings, 1991.

M. Barnett, R. Deline, M. Fähndrich, K. R. Leino, and W. Schulte, Verification of Object-Oriented Programs with Invariants., The Journal of Object Technology, vol.3, issue.6, 2004.
DOI : 10.5381/jot.2004.3.6.a2

R. Bornat, P. W. O-'hearn, C. Calcagno, and M. Parkinson, Permission accounting in separation logic, Principles of Programming Languages, 2005.

C. Boyapati, R. Lee, and M. Rinard, Ownership types for safe programming: Preventing data races and deadlocks, ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, 2002.

J. Boyland, Checking Interference with Fractional Permissions, Static Analysis Symposium, 2003.
DOI : 10.1007/3-540-44898-5_4

D. G. Clarke, J. M. Potter, and J. Noble, Ownership types for flexible alias protection, ACM Conference on Object- Oriented Programming Systems, Languages, and Applications, p.10, 1998.

F. S. De-boer, R. Deline, and M. Fähndrich, A sound and complete shared-variable concurrency model for multi-threaded Java programs Typestates for objects, International Conference on Formal Methods for Open Object-based Distributed Systems European Conference on Object-Oriented Programming, 2004.

A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv, Local Reasoning for Storable Locks and Threads, Asian Programming Languages and Systems Symposium, 2007.
DOI : 10.1007/978-3-540-76637-7_3

C. Haack, M. Huisman, and C. Hurlin, Reasoning about Java???s Reentrant Locks, 2008.
DOI : 10.1016/j.tcs.2006.12.035

C. Haack and C. Hurlin, Separation Logic Contracts for a Java-Like Language with Fork/Join, Algebraic Methodology and Software Technology, number 5140 in Lecture Notes in Computer Science, 2008.
DOI : 10.1007/978-3-540-79980-1_16
URL : https://hal.archives-ouvertes.fr/inria-00218114

A. Hobor, A. Appel, and F. Nardelli, Oracle Semantics for Concurrent Separation Logic, European Symposium on Programming, 2008.
DOI : 10.1007/978-3-540-78739-6_27
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.4226

S. Ishtiaq and P. W. O-'hearn, BI as an assertion language for mutable data structures, Principles of Programming Languages, 2001.

B. Jacobs, J. Smans, F. Piessens, and W. Schulte, A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs, International Conference on Formal Engineering Methods, 2006.
DOI : 10.1007/11901433_23

P. Müller, Modular Specification and Verification of Object-Oriented Programs, Lecture Notes in Computer Science, vol.2262, 2002.
DOI : 10.1007/3-540-45651-1

P. W. O-'hearn, Resources, concurrency and local reasoning, Theoretical Computer Science, vol.375, pp.1-3, 2007.

P. W. O-'hearn and D. J. Pym, The logic of bunched implications, Bulletin of Symbolic Logic, vol.5, issue.2, 1999.

M. Parkinson, Local Reasoning for Java, 2005.

M. Parkinson and G. Bierman, Separation logic and abstraction, Principles of Programming Languages, 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, 2002.
DOI : 10.1109/LICS.2002.1029817

P. Wadler, A taste of linear logic, Mathematical Foundations of Computer Science, 1993.
DOI : 10.1007/3-540-57182-5_12