{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T15:55:31Z","timestamp":1768406131409,"version":"3.49.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,5,31]],"date-time":"2017-05-31T00:00:00Z","timestamp":1496188800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s00224-016-9713-1","type":"journal-article","created":{"date-parts":[[2017,5,31]],"date-time":"2017-05-31T01:23:55Z","timestamp":1496193835000},"page":"371-461","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Separation Logic with One Quantified Variable"],"prefix":"10.1007","volume":"61","author":[{"given":"St\u00e9phane","family":"Demri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Didier","family":"Galmiche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9860-7203","authenticated-orcid":false,"given":"Dominique","family":"Larchey-Wendling","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"M\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,5,31]]},"reference":[{"key":"9713_CR1","doi-asserted-by":"crossref","unstructured":"Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: FOSSACS\u201914, Lecture Notes in Computer Science, vol. 8412, pp. 411\u2013425. Springer (2014)","DOI":"10.1007\/978-3-642-54830-7_27"},{"key":"9713_CR2","doi-asserted-by":"crossref","unstructured":"Bansal, K., Reynolds, A., King, T., Barrett, C., Wies, T.: Deciding local theory extensions via e-matching. In: CAV\u201915, Lecture Notes in Computer Science, vol. 9207, pp. 87\u2013105. Springer (2015)","DOI":"10.1007\/978-3-319-21668-3_6"},{"key":"9713_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV\u201911, Lecture Notes in Computer Science, vol. 8606, pp. 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9713_CR4","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.: Smallfoot: modular automatic assertion checking with separation logic. In: FMCO\u201905, Lecture Notes in Computer Science, vol. 4111, pp. 115\u2013137. Springer (2005)","DOI":"10.1007\/11804192_6"},{"issue":"3","key":"9713_CR5","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/j.apal.2009.07.004","volume":"161","author":"R Brochenin","year":"2009","unstructured":"Brochenin, R., Demri, S., Lozes, E.: Reasoning about sequences of memory states. Ann. Pure Appl. Logic 161(3), 305\u2013323 (2009)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9713_CR6","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1016\/j.ic.2011.12.003","volume":"211","author":"R Brochenin","year":"2012","unstructured":"Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106\u2013137 (2012)","journal-title":"Inf. Comput."},{"key":"9713_CR7","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Fuhs, C., Gorogiannis, N., Navarro Perez, J.: A decision procedure for satisfiability in separation logic with inductive predicates. In: CSL-LICS\u201914 (2014)","DOI":"10.1145\/2603088.2603091"},{"key":"9713_CR8","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. In: LICS\u201910, pp. 130\u2013139. IEEE (2010)","DOI":"10.1109\/LICS.2010.24"},{"key":"9713_CR9","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P., Yang, H.: Computability and complexity results for a spatial assertion language for data structures. In: FSTTCS\u201901, Lecture Notes in Computer Science, vol. 2245, pp. 108\u2013 119. Springer (2001)","DOI":"10.1007\/3-540-45294-X_10"},{"key":"9713_CR10","doi-asserted-by":"crossref","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: CONCUR\u201911, Lecture Notes in Computer Science, vol. 6901, pp. 235\u2013249. Springer (2011)","DOI":"10.1007\/978-3-642-23217-6_16"},{"issue":"3","key":"9713_CR11","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/j.ic.2006.10.006","volume":"205","author":"A Dawar","year":"2007","unstructured":"Dawar, A., Gardner, P., Ghelli, G.: Expressiveness and complexity of graph logic. Inf. Comput. 205(3), 263\u2013310 (2007)","journal-title":"Inf. Comput."},{"key":"9713_CR12","doi-asserted-by":"crossref","unstructured":"Demri, S., Deters, M.: Expressive completeness of separation logic with two variables and no separating conjunction. In: CSL-LICS\u201914. ACM Press (2014)","DOI":"10.1145\/2603088.2603142"},{"key":"9713_CR13","doi-asserted-by":"crossref","unstructured":"Demri, S., Galmiche, D., Larchey-Wendling, D., M\u00e9ry, D.: Separation logic with one quantified variable. In: CSR\u201914, Lecture Notes in Computer Science, vol. 8476, pp. 125\u2013138. Springer (2014)","DOI":"10.1007\/978-3-319-06686-8_10"},{"issue":"1","key":"9713_CR14","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1093\/logcom\/exn066","volume":"20","author":"D Galmiche","year":"2010","unstructured":"Galmiche, D., M\u00e9ry, D.: Tableaux and resource graphs for separation logic. J. Log. Comput. 20(1), 189\u2013231 (2010)","journal-title":"J. Log. Comput."},{"key":"9713_CR15","doi-asserted-by":"crossref","unstructured":"Haase, C., Ishtiaq, S., Ouaknine, J., Parkinson, M.: SeLoger: a tool for graph-based reasoning in separation logic. In: CAV\u201913, Lecture Notes in Computer Science, vol. 8044, pp. 790\u2013795. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_55"},{"key":"9713_CR16","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: CADE\u201913, Lecture Notes in Computer Science, vol. 7898, pp. 21\u201338. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"9713_CR17","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: Hankin, C., Schmidt, D. (eds.) POPL\u201901, pp. 14\u201326. ACM (2001)","DOI":"10.1145\/360204.375719"},{"key":"9713_CR18","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling, D., Galmiche, D.: The undecidability of Boolean BI through phase semantics. In: LICS\u201910, pp. 140\u2013149. IEEE (2010)","DOI":"10.1109\/LICS.2010.18"},{"key":"9713_CR19","unstructured":"Lozes, E.: Expressivit\u00e9 des logiques spatiales. Ph.D. Thesis, LIP, ENS Lyon, France (2004)"},{"key":"9713_CR20","unstructured":"Lozes, E.: Separation logic preserves the expressive power of classical logic. In: 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE\u201904) (2004)"},{"key":"9713_CR21","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f6rner, N.: Z3: an efficient SMT solver. In: TACAS\u201908, Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9713_CR22","doi-asserted-by":"crossref","unstructured":"P\u00e9rez, J. N., Rybalchenko, A.: Separation logic modulo theories. In: APLAS\u201913, Lecture Notes in Computer Science, vol. 8301, pp. 90\u2013106 (2013)","DOI":"10.1007\/978-3-319-03542-0_7"},{"key":"9713_CR23","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: CAV\u201913, Lecture Notes in Computer Science, vol. 2013, pp. 773\u2013789. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"9713_CR24","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: GRASShopper - complete heap verification with mixed specifications. In: TACAS\u201914, Lecture Notes in Computer Science, vol. 8413, pp. 124\u2013139. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"9713_CR25","unstructured":"Presburger, M.: \u00dcber Die Vollst\u00e4ndigkeit Eines Gewissen Systems Der Arithmetik Ganzer Zahlen, in Welchem Die Addition Als Einzige Operation Hervortritt. In: Comptes Rendus Du Premier Congr\u00e8s De Math\u00e9maticiens Des Pays Slaves, Warszawa, pp. 92\u2013101 (1929)"},{"key":"9713_CR26","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS\u201902, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-016-9713-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-016-9713-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-016-9713-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,25]],"date-time":"2019-09-25T04:29:10Z","timestamp":1569385750000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-016-9713-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,31]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["9713"],"URL":"https:\/\/doi.org\/10.1007\/s00224-016-9713-1","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5,31]]}}}