{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:29Z","timestamp":1763468189254,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,4,1]],"date-time":"2014-04-01T00:00:00Z","timestamp":1396310400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2014,4]]},"abstract":"<jats:p>\n            In this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in \u201cthe logic behind a fixed memory model\u201d, rather than in \u201ca model of any kind behind a given logical system\u201d. As an effective language for reasoning about such memory models, we use the formalism of separation logic. Our main result is that for any concrete choice of heap-like memory model, validity in that model is\n            <jats:italic>undecidable<\/jats:italic>\n            even for purely propositional formulas in this language.\n          <\/jats:p>\n          <jats:p>The main novelty of our approach to the problem is that we focus on validity in specific, concrete memory models, as opposed to validity in general classes of models.<\/jats:p>\n          <jats:p>Besides its intrinsic technical interest, this result also provides new insights into the nature of their decidable fragments. In particular, we show that, in order to obtain such decidable fragments, either the formula language must be severely restricted or the valuations of propositional variables must be constrained.<\/jats:p>\n          <jats:p>In addition, we show that a number of propositional systems that approximate separation logic are undecidable as well. In particular, this resolves the open problems of decidability for Boolean BI and Classical BI.<\/jats:p>\n          <jats:p>Moreover, we provide one of the simplest undecidable propositional systems currently known in the literature, called \u201cMinimal Boolean BI\u201d, by combining the purely positive implication-conjunction fragment of Boolean logic with the laws of multiplicative *-conjunction, its unit and its adjoint implication, originally provided by intuitionistic multiplicative linear logic. Each of these two components is individually decidable: the implication-conjunction fragment of Boolean logic is co-NP-complete, and intuitionistic multiplicative linear logic is NP-complete.<\/jats:p>\n          <jats:p>All of our undecidability results are obtained by means of a direct encoding of Minsky machines.<\/jats:p>","DOI":"10.1145\/2542667","type":"journal-article","created":{"date-parts":[[2014,4,22]],"date-time":"2014-04-22T13:37:45Z","timestamp":1398173865000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Undecidability of Propositional Separation Logic and Its Neighbours"],"prefix":"10.1145","volume":"61","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[{"name":"University College London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Max","family":"Kanovich","sequence":"additional","affiliation":[{"name":"University College London and Queen Mary, University of London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,4,24]]},"reference":[{"volume-title":"Proceedings of LICS-18","author":"Ahmed A.","key":"e_1_2_1_1_1","unstructured":"A. Ahmed , L. Jia , and D. Walker . 2003. Reasoning about hierarchical storage . In Proceedings of LICS-18 . IEEE Computer Society, 33--44. A. Ahmed, L. Jia, and D. Walker. 2003. Reasoning about hierarchical storage. In Proceedings of LICS-18. IEEE Computer Society, 33--44."},{"key":"e_1_2_1_2_1","unstructured":"A. V. Aho J. E. Hopcroft and J. D. Ullman. 1974. The Design and Analysis of Computer Algorithms. Addison-Wesley.   A. V. Aho J. E. Hopcroft and J. D. Ullman. 1974. The Design and Analysis of Computer Algorithms. Addison-Wesley."},{"volume-title":"The Theory of partitions. Encyclopedia of Mathematics and Its Applications","author":"Andrews G. E.","key":"e_1_2_1_3_1","unstructured":"G. E. Andrews . 1976. The Theory of partitions. Encyclopedia of Mathematics and Its Applications . Addison-Wesley . G. E. Andrews. 1976. The Theory of partitions. Encyclopedia of Mathematics and Its Applications. Addison-Wesley."},{"volume-title":"Proceedings of TLCA-1. Springer, 75--90","author":"Benton N. P.","key":"e_1_2_1_4_1","unstructured":"N. P. Benton , G. M. Bierman , V. de Paiva , and M. Hyland . 1993. A term calculus for intuitionistic linear logic . In Proceedings of TLCA-1. Springer, 75--90 . N. P. Benton, G. M. Bierman, V. de Paiva, and M. Hyland. 1993. A term calculus for intuitionistic linear logic. In Proceedings of TLCA-1. Springer, 75--90."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-012-9449-0"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(3:3)2010"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.24"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535844"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/646839.708666"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02283036"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_33"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004858"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103663"},{"volume-title":"Proceedings of TAPSOFT'87","author":"Girard J.-Y.","key":"e_1_2_1_20_1","unstructured":"J.-Y. Girard and Y. Lafont . 1987. Linear logic and lazy computation . In Proceedings of TAPSOFT'87 . Springer-Verlag, 52--66. J.-Y. Girard and Y. Lafont. 1987. Linear logic and lazy computation. In Proceedings of TAPSOFT'87. Springer-Verlag, 52--66."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480886"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1992.185533"},{"volume-title":"Advances in Linear Logic","author":"Kanovich M.","key":"e_1_2_1_25_1","unstructured":"M. Kanovich . 1995. The direct simulation of Minsky machines in linear logic . In Advances in Linear Logic , London Mathematical Society Lecture Notes Series, vol. 222 , Cambridge University Press , 123--145. M. Kanovich. 1995. The direct simulation of Minsky machines in linear logic. In Advances in Linear Logic, London Mathematical Society Lecture Notes Series, vol. 222, Cambridge University Press, 123--145."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01049412"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.18"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422085.2422091"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328451"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.52"},{"volume-title":"Petri Net Theory and the Modeling of Systems","author":"Peterson J. L.","key":"e_1_2_1_35_1","unstructured":"J. L. Peterson . 1981. Petri Net Theory and the Modeling of Systems . Prentice-Hall . J. L. Peterson. 1981. Petri Net Theory and the Modeling of Systems. Prentice-Hall."},{"key":"e_1_2_1_36_1","series-title":"Applied Logic Series","volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","author":"Pym D.","unstructured":"D. Pym . 2002. The Semantics and Proof Theory of the Logic of Bunched Implications . Applied Logic Series . Kluwer . D. Pym. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90006-9"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2542667","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2542667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:10:07Z","timestamp":1750234207000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2542667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["10.1145\/2542667"],"URL":"https:\/\/doi.org\/10.1145\/2542667","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2014,4]]},"assertion":[{"value":"2012-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-04-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}