E. Ptime, (I)) coNP-C. (Th, p.1414

. Acknowledgements, We thanks the anonymous referees for their remarks and suggestions

R. Barrett, S. Sebastiani, C. Seshia, and . Tinelli, Satisfiability Modulo Theories, Frontiers in Artificial Intelligence and Applications, vol.185, pp.825-885, 2008.
URL : https://hal.archives-ouvertes.fr/hal-01095009

C. Berdine, P. O. Calcagno, and . Hearn, A Decidable Fragment of Separation Logic, FSTTCS'04, pp.97-109, 2004.
DOI : 10.1007/978-3-540-30538-5_9

C. Bornat, P. O. Calcagno, M. Hearn, and . Parkinson, Permission accounting in separation logic, POPL'05, pp.259-270, 2005.
DOI : 10.1145/1040305.1040327

. Boyland, Checking Interference with Fractional Permissions, SAS'03, number 2694 in LNCS, pp.55-72, 2003.
DOI : 10.1007/3-540-44898-5_4
URL : http://www.cs.uwm.edu/~boyland/papers/permissions.pdf

C. Cook, J. Haase, M. Ouaknine, J. Parkinson, and . Worrell, Tractable Reasoning in a Fragment of Separation Logic, CONCUR'11, pp.235-249, 2011.
DOI : 10.1007/3-540-45294-X_10

A. Dockins, A. W. Hobor, and . Appel, A Fresh Look at Separation Algebras and Share Accounting, APLAS'09, pp.161-177, 2009.
DOI : 10.1007/978-3-642-10672-9_13
URL : http://www.cs.princeton.edu/~aahobor/fresh-sa.pdf

D. Galmiche, D. Mery, and . Pym, Resource tableaux (extended abstract), CSL'02, pp.183-199, 2002.
DOI : 10.1007/3-540-45793-3_13
URL : https://hal.archives-ouvertes.fr/inria-00100798

D. S. Garey and . Johnson, Computers and intractability: a guide to the theory of NPcompleteness, Freeman, 1979.

S. Haase, J. Ishtiaq, M. Ouaknine, and . Parkinson, SeLoger: A Tool for Graph-Based Reasoning in Separation Logic, CAV'13, pp.790-795, 2013.
DOI : 10.1007/978-3-642-39799-8_55

S. He, C. Qin, W. N. Luo, and . Chin, Memory Usage Verification Using Hip/Sleek, ATVA'09, number 5799 in LNCS, pp.166-181, 2009.
DOI : 10.1007/978-3-642-04761-9_14
URL : http://www.comp.nus.edu.sg/~chinwn/papers/atva09.pdf

J. Jacobs, P. Smans, F. Philippaerts, W. Vogels, F. Penninckx et al., VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, NFM'11, pp.41-55, 2011.
DOI : 10.1007/11691372_19

C. Bach-le, A. Gherghina, and . Hobor, Decision procedures over sophisticated fractional permissions, APLAS'12, pp.368-385, 2012.

C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.55-74, 2002.
DOI : 10.1109/LICS.2002.1029817
URL : http://ttic.uchicago.edu/~dreyer/seplogic.pdf

. Th and . Schaefer, The complexity of satisfiability problems, STOC'78, pp.216-226, 1978.

E. Villard, C. Lozes, and . Calcagno, Tracking Heaps That Hop with Heap-Hop, TACAS'10, pp.275-279, 2010.
DOI : 10.1007/978-3-642-12002-2_23
URL : http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VLC-tacas10.pdf