{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:27Z","timestamp":1763468187073,"version":"3.40.4"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319066851"},{"type":"electronic","value":"9783319066868"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06686-8_10","type":"book-chapter","created":{"date-parts":[[2014,6,2]],"date-time":"2014-06-02T05:30:40Z","timestamp":1401687040000},"page":"125-138","source":"Crossref","is-referenced-by-count":15,"title":["Separation Logic with One Quantified Variable"],"prefix":"10.1007","author":[{"given":"St\u00e9phane","family":"Demri","sequence":"first","affiliation":[]},{"given":"Didier","family":"Galmiche","sequence":"additional","affiliation":[]},{"given":"Dominique","family":"Larchey-Wendling","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"M\u00e9ry","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"issue":"3","key":"10_CR3","first-page":"305","volume":"161","author":"R. Brochenin","year":"2009","unstructured":"Brochenin, R., Demri, S., Lozes, E.: Reasoning about sequences of memory states. APAL\u00a0161(3), 305\u2013323 (2009)","journal-title":"APAL"},{"key":"10_CR4","first-page":"106","volume":"211","author":"R. Brochenin","year":"2012","unstructured":"Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. IC\u00a0211, 106\u2013137 (2012)","journal-title":"IC"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. In: LICS 2010, pp. 130\u2013139. IEEE (2010)","DOI":"10.1109\/LICS.2010.24"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C. Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 108\u2013119. Springer, Heidelberg (2001)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B. Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 235\u2013249. Springer, Heidelberg (2011)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"10_CR9","unstructured":"Demri, S., Deters, M.: Two-variable separation logic and its inner circle (September 2013) (submitted)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Demri, S., Galmiche, D., Larchey-Wendling, D., Mery, D.: Separation logic with one quantified variable. arXiv (2014)","DOI":"10.1007\/978-3-319-06686-8_10"},{"issue":"1","key":"10_CR11","first-page":"189","volume":"20","author":"D. Galmiche","year":"2010","unstructured":"Galmiche, D., M\u00e9ry, D.: Tableaux and resource graphs for separation logic. JLC\u00a020(1), 189\u2013231 (2010)","journal-title":"JLC"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"790","DOI":"10.1007\/978-3-642-39799-8_55","volume-title":"Computer Aided Verification","author":"C. Haase","year":"2013","unstructured":"Haase, C., Ishtiaq, S., Ouaknine, J., Parkinson, M.J.: SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 790\u2013795. Springer, Heidelberg (2013)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-38574-2_2","volume-title":"Automated Deduction \u2013 CADE-24","author":"R. Iosif","year":"2013","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 21\u201338. Springer, Heidelberg (2013)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: POPL 2001, pp. 14\u201326 (2001)","DOI":"10.1145\/373243.375719"},{"issue":"3","key":"10_CR15","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. Ladner","year":"1977","unstructured":"Ladner, R.: The computational complexity of provability in systems of modal propositional logic. SIAM Journal of Computing\u00a06(3), 467\u2013480 (1977)","journal-title":"SIAM Journal of Computing"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling, D., Galmiche, D.: The undecidability of boolean BI through phase semantics. In: LICS 2010, pp. 140\u2013149. IEEE (2010)","DOI":"10.1109\/LICS.2010.18"},{"key":"10_CR17","unstructured":"Lozes, E.: Expressivit\u00e9 des logiques spatiales. PhD thesis, LIP, ENS Lyon, France (2004)"},{"key":"10_CR18","unstructured":"Lozes, E.: Separation logic preserves the expressive power of classical logic. In: Workshop SPACE 2004 (2004)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","volume-title":"Computer Aided Verification","author":"R. Piskac","year":"2013","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 773\u2013789. Springer, Heidelberg (2013)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"}],"container-title":["Lecture Notes in Computer Science","Computer Science - Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06686-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T05:49:05Z","timestamp":1746251345000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06686-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319066851","9783319066868"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06686-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}