{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T04:56:57Z","timestamp":1763182617964,"version":"3.37.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030027674"},{"type":"electronic","value":"9783030027681"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02768-1_18","type":"book-chapter","created":{"date-parts":[[2018,10,21]],"date-time":"2018-10-21T07:42:27Z","timestamp":1540107747000},"page":"329-349","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["On the Complexity of Pointer Arithmetic in Separation Logic"],"prefix":"10.1007","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[]},{"given":"Max","family":"Kanovich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,22]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/978-3-642-54830-7_27","volume-title":"Foundations of Software Science and Computation Structures","author":"T Antonopoulos","year":"2014","unstructured":"Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 411\u2013425. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54830-7_27"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97\u2013109. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30538-5_9"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-22110-1_15","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2011","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178\u2013183. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_15"},{"key":"18_CR4","doi-asserted-by":"publisher","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":"18_CR5","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Fuhs, C., Gorogiannis, N., Navarro P\u00e9rez, J.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of the CSL-LICS, pp. 25:1\u201325:10. ACM (2014)","DOI":"10.1145\/2603088.2603091"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-319-63046-5_29","volume-title":"Automated Deduction \u2013 CADE 26","author":"J Brotherston","year":"2017","unstructured":"Brotherston, J., Gorogiannis, N., Kanovich, M.: Biabduction (and related problems) in array separation logic. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 472\u2013490. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_29"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Gorogiannis, N., Kanovich, M., Rowe, R.: Model checking for symbolic-heap separation logic with inductive predicates. In: Proceedings of the POPL-43, pp. 84\u201396. ACM (2016)","DOI":"10.1145\/2837614.2837621"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-17524-9_1","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2015","unstructured":"Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3\u201311. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1"},{"key":"18_CR9","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., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108\u2013119. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45294-X_10"},{"key":"18_CR10","unstructured":"Chen, T., Song, F., Wu, Z.: Tractability of separation logic with inductive definitions: beyond lists. In: Proceedings of the CONCUR-28, pp. 33:1\u201333:16. Dagstuhl (2017)"},{"key":"18_CR11","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. 6901, pp. 235\u2013249. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23217-6_16"},{"key":"18_CR12","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)","edition":"3"},{"key":"18_CR13","unstructured":"Demri, S., Lozes, E., Lugiez, D.: On symbolic heaps modulo permission theories. In: Proceedings of the FSTTCS-37, pp. 25:1\u201325:13. Dagstuhl (2017)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-319-89366-2_26","volume-title":"Foundations of Software Science and Computation Structures","author":"S Demri","year":"2018","unstructured":"Demri, S., Lozes, \u00c9., Mansutti, A.: The effects of adding reachability predicates in propositional separation logic. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 476\u2013493. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_26"},{"key":"18_CR15","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"MR Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, New York (1979)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-319-40229-1_36","volume-title":"Automated Reasoning","author":"X Gu","year":"2016","unstructured":"Gu, X., Chen, T., Wu, Z.: A complete decision procedure for linearly compositional separation logic with data constraints. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 532\u2013549. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_36"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Haase, C.: Subclasses of Presburger arithmetic and the weak EXP hierarchy. In: Proceedings of CSL-LICS, pp. 47:1\u201347:10. ACM (2014)","DOI":"10.1145\/2603088.2603092"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 7898, pp. 21\u201338. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_2"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-319-71237-6_9","volume-title":"Programming Languages and Systems","author":"D Kimura","year":"2017","unstructured":"Kimura, D., Tatsuta, M.: Decision procedure for entailment of symbolic heaps with arrays. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 169\u2013189. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_9"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-41528-4_21","volume-title":"Computer Aided Verification","author":"QL Le","year":"2016","unstructured":"Le, Q.L., Sun, J., Chin, W.-N.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 382\u2013404. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_21"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-319-63390-9_26","volume-title":"Computer Aided Verification","author":"QL Le","year":"2017","unstructured":"Le, Q.L., Tatsuta, M., Sun, J., Chin, W.-N.: A decidable fragment in separation logic with\u00a0inductive predicates and arithmetic. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 495\u2013517. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_26"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-35182-2_26","volume-title":"Programming Languages and Systems","author":"XB Le","year":"2012","unstructured":"Le, X.B., Gherghina, C., Hobor, A.: Decision procedures over sophisticated fractional permissions. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 368\u2013385. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35182-2_26"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the LICS-17, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"1","key":"18_CR24","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1090\/S0002-9947-1984-0742421-9","volume":"284","author":"B Scarpellini","year":"1984","unstructured":"Scarpellini, B.: Complexity of subcases of Presburger arithmetic. Trans. Am. Math. Soc. 284(1), 203\u2013218 (1984)","journal-title":"Trans. Am. Math. Soc."},{"key":"18_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"LJ Stockmeyer","year":"1977","unstructured":"Stockmeyer, L.J.: The polynomial-time hierarchy. Theor. Comput. Sci. 3, 1\u201322 (1977)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H Yang","year":"2008","unstructured":"Yang, H., et al.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385\u2013398. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_36"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/3-540-45931-6_28","volume-title":"Foundations of Software Science and Computation Structures","author":"H Yang","year":"2002","unstructured":"Yang, H., O\u2019Hearn, P.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 402\u2013416. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45931-6_28"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02768-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T06:11:31Z","timestamp":1572156691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02768-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030027674","9783030027681"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02768-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Wellington","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/aplas2018.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}