A. Aiken and A. Nicolau, Optimal loop parallelization, ACM SIGPLAN Notices, vol.23, issue.7, 1988.

P. Artigas, M. Gupta, S. Midkiff, and J. Moreira, Automatic loop transformations and parallelization for Java, International Conference on Supercomputing, 2000.

E. Balland, P. Brauner, R. Kopetz, P. Moreau, and A. Reilles, Tom: Piggybacking Rewriting on Java, Rewriting Techniques and Applications, 2007.
DOI : 10.1007/978-3-540-73449-9_5
URL : https://hal.archives-ouvertes.fr/inria-00142045

G. Barthe, B. Grégoire, C. Kunz, and T. Rezk, Certificate translation for optimizing compilers, Static Analysis Symposium, number 4134 in Lecture Notes in Computer Science, 2006.
DOI : 10.1145/1538917.1538919

J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. W. O-'hearn et al., Shape Analysis for Composite Data Structures, Conference on Computer Aided Verification of Lecture Notes in Computer Science, 2007.
DOI : 10.1007/978-3-540-73368-3_22

J. Berdine, C. Calcagno, and P. W. O-'hearn, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, Formal Methods for Components and Objects of Lecture Notes in Computer Science, 2005.
DOI : 10.1007/11804192_6

J. Berdine, C. Calcagno, and P. W. O-'hearn, Symbolic Execution with Separation Logic, Asian Programming Languages and Systems Symposium, 2005.
DOI : 10.1007/11575467_5

A. Bik and D. Gannon, Automatically exploiting implicit parallelism in Java, Concurrency: Practice and Experience, 1997.

R. Bornat, C. Calcagno, and H. Yang, Variables as Resource in Separation Logic, Mathematical Foundations of Programming Semantics, 2005.
DOI : 10.1016/j.entcs.2005.11.059

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

C. Calcagno, D. Distefano, P. Ohearn, and H. Yang, Compositional shape analysis by means of bi-abduction, Principles of Programming Languages, 2009.

W. Chin, C. David, H. Nguyen, and S. Qin, Enhancing modular OO verification with separation logic, Principles of Programming Languages, 2008.

D. Cunningham, K. Gudka, and S. Eisenbach, Keep Off the Grass: Locking the Right Path for Atomicity, International Conference on Compiler Construction, 2008.
DOI : 10.1007/978-3-540-78791-4_19

D. Distefano, P. W. O-'hearn, and H. Yang, A Local Shape Analysis Based on Separation Logic, Tools and Algorithms for the Construction and Analysis of Systems, 2006.
DOI : 10.1145/514188.514190

D. Distefano and M. Parkinson, jStar: Towards practical verification for Java, ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, 2008.

O. Ergin, D. Balkan, D. Ponomarev, and K. Ghose, Early Register Deallocation Mechanisms Using Checkpointed Register Files, IEEE Computer, 2006.
DOI : 10.1109/TC.2006.145

R. Ghiya, L. J. Hendren, and Y. Zhu, Detecting parallelism in C programs with recursive data structures, International Conference on Compiler Construction, 1998.
DOI : 10.1007/BFb0026429

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

R. Gupta, S. Pande, K. Psarris, and V. Sarkar, Compilation techniques for parallel systems, Parallel Computing, vol.25, issue.13-14, p.25, 1999.
DOI : 10.1016/S0167-8191(99)00086-1

C. Haack, M. Huisman, and C. Hurlin, Reasoning about Java???s Reentrant Locks, Asian Programming Languages and Systems Symposium, 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, 2008.
DOI : 10.1007/978-3-540-79980-1_16
URL : https://hal.archives-ouvertes.fr/inria-00218114

L. J. Hendren and A. Nicolau, Parallelizing programs with recursive data structures, IEEE Transactions on Parallel and Distributed Systems, vol.1, issue.1, p.1, 1990.
DOI : 10.1109/71.80123

B. Jacobs and F. Piessens, The verifast program verifier, 2008.

G. Jin, J. Mellor-crummey, and R. Fowler, Increasing temporal locality with skewing and recursive blocking, Proceedings of the 2001 ACM/IEEE conference on Supercomputing (CDROM) , Supercomputing '01, 2001.
DOI : 10.1145/582034.582077

L. Lamport, The parallel execution of DO loops, Communications of the ACM, vol.17, issue.2, 1974.
DOI : 10.1145/360827.360844

X. Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Principles of Programming Languages, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

G. C. Necula, Translation validation for an optimizing compiler, ACM SIGPLAN Notices, vol.35, issue.5, 2000.

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

P. W. O-'hearn, J. Reynolds, and H. Yang, Local reasoning about programs that alter data structures, Computer Science Logic Lecture Notes in Computer Science, vol.2142, 2001.

M. Parkinson, Local Reasoning for Java, 2005.

M. Raza, C. Calcagno, and P. Gardner, Automatic Parallelization with Separation Logic, European Symposium on Programming, 2009.
DOI : 10.1007/978-3-642-00590-9_25

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

M. Snir and J. Yu, On the theory of spatial and temporal locality, 2005.

M. Strecker, Formal Verification of a Java Compiler in Isabelle, Conference on Automated Deduction, 2002.
DOI : 10.1007/3-540-45620-1_5

C. Xue, Z. Shao, and E. Sha, Maximize Parallelism Minimize Overhead for Nested Loops via Loop Striping, The Journal of VLSI Signal Processing Systems for Signal, Image, and Video Technology, vol.2, issue.4, 2004.
DOI : 10.1007/s11265-006-0034-5