{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T16:59:29Z","timestamp":1768409969528,"version":"3.49.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,3,21]],"date-time":"2015-03-21T00:00:00Z","timestamp":1426896000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011102","name":"EU Seventh Framework Programme","doi-asserted-by":"crossref","award":["PIOF-GA-2011-301166 (DATAVERIF)"],"award-info":[{"award-number":["PIOF-GA-2011-301166 (DATAVERIF)"]}],"id":[{"id":"10.13039\/100011102","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Science Foundation","award":["0644299"],"award-info":[{"award-number":["0644299"]}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,3,21]]},"abstract":"<jats:p>Separation logic is a well-known assertion language for Hoare-style proof systems. We show that first-order separation logic with a unique record field restricted to two quantified variables and no program variables is undecidable. This is among the smallest fragments of separation logic known to be undecidable, and this contrasts with the decidability of two-variable first-order logic. We also investigate its restriction by dropping the magic wand connective, known to be decidable with nonelementary complexity, and we show that the satisfiability problem with only two quantified variables is not yet elementary recursive. Furthermore, we establish insightful and concrete relationships between two-variable separation logic and propositional interval temporal logic (PITL), data logics, and modal logics, providing an inner circle of closely related logics.<\/jats:p>","DOI":"10.1145\/2724711","type":"journal-article","created":{"date-parts":[[2015,4,22]],"date-time":"2015-04-22T13:57:35Z","timestamp":1429711055000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Two-Variable Separation Logic and Its Inner Circle"],"prefix":"10.1145","volume":"16","author":[{"given":"St\u00e9phane","family":"Demri","sequence":"first","affiliation":[{"name":"New York University &amp; CNRS, France"}]},{"given":"Morgan","family":"Deters","sequence":"additional","affiliation":[{"name":"New York University, New York, NY, USA"}]}],"member":"320","published-online":{"date-parts":[[2015,4,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/182.358434"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/3266641.3266646"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_10"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"P. Blackburn M. de Rijke and Y. Venema. 2001. Modal Logic. Cambridge University Press. P. Blackburn M. de Rijke and Y. Venema. 2001. Modal Logic. Cambridge University Press.","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1970398.1970403"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"E. B\u00f6rger E. Gr\u00e4del and Y. Gurevich. 1997. The Classical Decision Problem. Springer. E. B\u00f6rger E. Gr\u00e4del and Y. Gurevich. 1997. The Classical Decision Problem. Springer.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(02)00229-6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.12.003"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603091"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2542667"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"C. Calcagno P. O\u2019Hearn and H. Yang. 2001. Computability and complexity results for a spatial assertion language for data structures. In FSTTCS\u201901 (Lecture Notes in Computer Science) Vol. 2245. Springer 108--119. C. Calcagno P. O\u2019Hearn and H. Yang. 2001. Computability and complexity results for a spatial assertion language for data structures. In FSTTCS\u201901 (Lecture Notes in Computer Science) Vol. 2245. Springer 108--119.","DOI":"10.1007\/3-540-45294-X_10"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603134"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"B. Cook Ch. Haase J. Ouaknine M. Parkinson and J. Worrell. 2011. Tractable reasoning in a fragment of separation logic. In CONCUR\u201911 (Lecture Notes in Computer Science). Springer 235--249. B. Cook Ch. Haase J. Ouaknine M. Parkinson and J. Worrell. 2011. Tractable reasoning in a fragment of separation logic. In CONCUR\u201911 (Lecture Notes in Computer Science). Springer 235--249.","DOI":"10.1007\/978-3-642-23217-6_16"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"J.-R. Courtault and D. Galmiche. 2013. A modal BI logic for dynamic resource properties. In LFCS\u201913 (Lecture Notes in Computer Science) Vol. 7734. Springer 134--148. J.-R. Courtault and D. Galmiche. 2013. A modal BI logic for dynamic resource properties. In LFCS\u201913 (Lecture Notes in Computer Science) Vol. 7734. Springer 134--148.","DOI":"10.1007\/978-3-642-35722-0_10"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.10.006"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275293"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"N. Decker P. Habermehl M. Leucker and D. Thoma. 2014. Ordered navigation on multi-attributed data words. In CONCUR\u201914 (Lecture Notes in Computer Science) Vol. 8704. 497--511. N. Decker P. Habermehl M. Leucker and D. Thoma. 2014. Ordered navigation on multi-attributed data words. In CONCUR\u201914 (Lecture Notes in Computer Science) Vol. 8704. 497--511.","DOI":"10.1007\/978-3-662-44584-6_34"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021352309671"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603142"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"S. Demri D. Galmiche D. Larchey-Wendling and D. Mery. 2014. Separation logic with one quantified variable. In CSR\u201914 (Lecture Notes in Computer Science) Vol. 8476. Springer 125--138. S. Demri D. Galmiche D. Larchey-Wendling and D. Mery. 2014. Separation logic with one quantified variable. In CSR\u201914 (Lecture Notes in Computer Science) Vol. 8476. Springer 125--138.","DOI":"10.1007\/978-3-319-06686-8_10"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3094"},{"key":"e_1_2_1_23_1","volume-title":"LICS\u201997","author":"Etessami K.","unstructured":"K. Etessami , M. Vardi , and Th. Wilke . 1997. First-order logic with two variables and unary temporal logics . In LICS\u201997 . IEEE , 228--235. K. Etessami, M. Vardi, and Th. Wilke. 1997. First-order logic with two variables and unary temporal logics. In LICS\u201997. IEEE, 228--235."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"D. Gabbay. 1981. Expressive functional completeness in tense logic. In Aspects of Philosophical Logic. Reidel 91--117. D. Gabbay. 1981. Expressive functional completeness in tense logic. In Aspects of Philosophical Logic. Reidel 91--117.","DOI":"10.1007\/978-94-009-8384-7_4"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275098"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.2307\/421196"},{"key":"e_1_2_1_28_1","unstructured":"E. Gr\u00e4del M. Otto and E. Rosen. 1997b. Two-variable logic with counting is decidable. In LICS\u201997. IEEE 306--317. E. Gr\u00e4del M. Otto and E. Rosen. 1997b. Two-variable logic with counting is decidable. In LICS\u201997. IEEE 306--317."},{"key":"e_1_2_1_29_1","first-page":"4","article-title":"Undecidability results on two-variable logics","volume":"38","author":"Gr\u00e4del E.","year":"1999","unstructured":"E. Gr\u00e4del , M. Otto , and E. Rosen . 1999 . Undecidability results on two-variable logics . Archive for Mathematical Logic 38 , 4 -- 5 (1999), 313--354. E. Gr\u00e4del, M. Otto, and E. Rosen. 1999. Undecidability results on two-variable logics. Archive for Mathematical Logic 38, 4--5 (1999), 313--354.","journal-title":"Archive for Mathematical Logic"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(95)00018-A"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"D. Harel D. Kozen and J. Tiuryn. 2000. Dynamic Logic. MIT Press. D. Harel D. Kozen and J. Tiuryn. 2000. Dynamic Logic. MIT Press.","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"M. Hennessy and R. Milner. 1980. On observing nondeterminism and concurrency. In ICALP\u201980 (Lecture Notes in Computer Science) Vol. 85. Springer 299--309. M. Hennessy and R. Milner. 1980. On observing nondeterminism and concurrency. In ICALP\u201980 (Lecture Notes in Computer Science) Vol. 85. Springer 299--309.","DOI":"10.1007\/3-540-10003-2_79"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.48.3.365"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.53"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422085.2422091"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"C. Lutz and U. Sattler. 2002. The complexity of reasoning with Boolean modal logics. In Advances in Modal Logics 2000. Vol. 3. World Scientific 329--348. C. Lutz and U. Sattler. 2002. The complexity of reasoning with Boolean modal logics. In Advances in Modal Logics 2000. Vol. 3. World Scientific 329--348.","DOI":"10.1142\/9789812776471_0018"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1976.1674704"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.14.55-104"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.2307\/2695037"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"L. Pacholski W. Szwast and L. Tendera. 1997. Complexity of two-variable logic with counting. In LICS\u201997. IEEE 318--327. L. Pacholski W. Szwast and L. Tendera. 1997. Complexity of two-variable logic with counting. In LICS\u201997. IEEE 318--327.","DOI":"10.1109\/LICS.1997.614958"},{"key":"e_1_2_1_46_1","volume-title":"Present and Future","author":"Prior A.","unstructured":"A. Prior . 1967. Past , Present and Future . Oxford University Press . A. Prior. 1967. Past, Present and Future. Oxford University Press."},{"key":"e_1_2_1_47_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"41","author":"Rabin M.","year":"1969","unstructured":"M. Rabin . 1969 . Decidability of second-order theories and automata on infinite trees . Transactions on the American Mathematics Society 41 (1969), 1 -- 35 . M. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Transactions on the American Mathematics Society 41 (1969), 1--35.","journal-title":"Transactions on the American Mathematics Society"},{"key":"e_1_2_1_48_1","volume-title":"LICS\u201902","author":"Reynolds J. C.","unstructured":"J. C. Reynolds . 2002. Separation logic: A logic for shared mutable data structures . In LICS\u201902 . IEEE , 55--74. J. C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS\u201902. IEEE, 55--74."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:15)2012"},{"key":"e_1_2_1_50_1","first-page":"377","article-title":"A decision method for validity of sentences in two variables","volume":"27","author":"Scott D.","year":"1962","unstructured":"D. Scott . 1962 . A decision method for validity of sentences in two variables . Journal of Symbolic Logic 27 (1962), 377 . D. Scott. 1962. A decision method for validity of sentences in two variables. Journal of Symbolic Logic 27 (1962), 377.","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_2_1_52_1","unstructured":"W. Szwast and L. Tendera. 2013. FO2 with one transitive relation is decidable. In STACS\u201913 (LIPIcs) Vol. 20. 317--328. W. Szwast and L. Tendera. 2013. FO2 with one transitive relation is decidable. In STACS\u201913 (LIPIcs) Vol. 20. 317--328."},{"key":"e_1_2_1_56_1","unstructured":"Z. Chaochen. 2008. In Logics of Specification Languages D. Bjorner and M. Henson (Eds.). Springer Chapter Reviews on \u201cDuration Calculus \u201d 609--611. Monographs in Theoretical Computer Science. An EATCS Series. Z. Chaochen. 2008. In Logics of Specification Languages D. Bjorner and M. Henson (Eds.). Springer Chapter Reviews on \u201cDuration Calculus \u201d 609--611. Monographs in Theoretical Computer Science. An EATCS Series."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2724711","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2724711","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:12:12Z","timestamp":1750227132000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2724711"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,21]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,3,21]]}},"alternative-id":["10.1145\/2724711"],"URL":"https:\/\/doi.org\/10.1145\/2724711","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,21]]},"assertion":[{"value":"2013-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-04-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}