{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:05:33Z","timestamp":1770275133854,"version":"3.49.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319630458","type":"print"},{"value":"9783319630465","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_29","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:34:07Z","timestamp":1499679247000},"page":"472-490","source":"Crossref","is-referenced-by-count":11,"title":["Biabduction (and Related Problems) in Array Separation Logic"],"prefix":"10.1007","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[]},{"given":"Nikos","family":"Gorogiannis","sequence":"additional","affiliation":[]},{"given":"Max","family":"Kanovich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"issue":"3","key":"29_CR1","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1006\/jcss.1999.1691","volume":"60","author":"M Ajtai","year":"2000","unstructured":"Ajtai, M., Fagin, R., Stockmeyer, L.J.: The closure of monadic NP. J. Comput. Syst. Sci. 60(3), 660\u2013716 (2000)","journal-title":"J. Comput. Syst. Sci."},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-54862-8_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Alberti","year":"2014","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 15\u201330. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_2"},{"key":"29_CR3","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). doi: 10.1007\/978-3-642-54830-7_27"},{"key":"29_CR4","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). doi: 10.1007\/978-3-540-30538-5_9"},{"key":"29_CR5","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). doi: 10.1007\/978-3-642-22110-1_15"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-04081-8_13","volume-title":"CONCUR 2009 - Concurrency Theory","author":"A Bouajjani","year":"2009","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 178\u2013195. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04081-8_13"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-33386-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 167\u2013182. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33386-6_14"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2005). doi: 10.1007\/11609773_28"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-74061-2_6","volume-title":"Static Analysis","author":"J Brotherston","year":"2007","unstructured":"Brotherston, J.: Formalised inductive reasoning in the logic of bunched implications. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 87\u2013103. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74061-2_6"},{"key":"29_CR10","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 CSL-LICS, pp. 25:1\u201325:10. ACM (2014)","DOI":"10.1145\/2603088.2603091"},{"key":"29_CR11","unstructured":"Brotherston, J., Gorogiannis, N., Kanovich, M.: Biabduction (and related problems) in array separation logic. CoRR abs\/1607.01993 (2016). http:\/\/arxiv.org\/abs\/1607.01993"},{"key":"29_CR12","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 POPL-43, pp. 84\u201396. ACM (2016)","DOI":"10.1145\/2837614.2837621"},{"key":"29_CR13","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., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3\u201311. Springer, Cham (2015). doi: 10.1007\/978-3-319-17524-9_1"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6) (2011)","DOI":"10.1145\/2049697.2049700"},{"issue":"9","key":"29_CR15","doi-asserted-by":"crossref","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"WN Chin","year":"2012","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comp. Prog. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comp. Prog."},{"key":"29_CR16","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). doi: 10.1007\/978-3-642-23217-6_16"},{"key":"29_CR17","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":"29_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-35873-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2013","unstructured":"Cousot, P., Cousot, R., F\u00e4hndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 128\u2013148. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35873-9_10"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of POPL-38, pp. 105\u2013118. ACM (2011)","DOI":"10.1145\/1926385.1926399"},{"key":"29_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-11957-6_14","volume-title":"Programming Languages and Systems","author":"I Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 246\u2013266. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11957-6_14"},{"key":"29_CR21","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":"29_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-642-23702-7_7","volume-title":"Static Analysis","author":"N Gorogiannis","year":"2011","unstructured":"Gorogiannis, N., Kanovich, M., O\u2019Hearn, P.W.: The complexity of abduction for separated heap abstractions. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 25\u201342. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23702-7_7"},{"key":"29_CR23","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0304-3975(88)90136-3","volume":"56","author":"E Gr\u00e4del","year":"1988","unstructured":"Gr\u00e4del, E.: Subclasses of Presburger arithmetic and the polynomial-time hierarchy. Theor. Comput. Sci. 56, 289\u2013301 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR24","series-title":"Lecture Notes in Computer Science","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, vol. 9706, pp. 532\u2013549. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1_36"},{"key":"29_CR25","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"},{"issue":"2","key":"29_CR26","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/S0019-9958(85)80004-8","volume":"65","author":"J Hartmanis","year":"1985","unstructured":"Hartmanis, J., Immerman, N., Sewelson, V.: Sparse sets in NP-P: EXPTIME versus NEXPTIME. Inform. Control 65(2), 158\u2013181 (1985)","journal-title":"Inform. Control"},{"key":"29_CR27","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. 7898, pp. 21\u201338. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38574-2_2"},{"key":"29_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-20398-5_4"},{"key":"29_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470\u2013485. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00593-0_33"},{"key":"29_CR30","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). doi: 10.1007\/978-3-319-41528-4_21"},{"key":"29_CR31","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers., A.J.: Automatic verification of iterated separating conjunctions using symbolic execution. In: Proceedings of CAV-28 (2016, to appear)","DOI":"10.1007\/978-3-319-41528-4_22"},{"issue":"1\u20133","key":"29_CR32","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR33","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proceedings of POPL-31, pp. 268\u2013280. ACM (2004)","DOI":"10.1145\/982962.964024"},{"key":"29_CR34","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS-17, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"1","key":"29_CR35","doi-asserted-by":"crossref","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":"29_CR36","doi-asserted-by":"crossref","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."},{"issue":"1","key":"29_CR37","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s10817-016-9389-x","volume":"58","author":"T Str\u00f6der","year":"2017","unstructured":"Str\u00f6der, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P., Aschermann, C.: Automatically proving termination and memory safety for programs with pointer arithmetic. J. Autom. Reasoning 58(1), 33\u201365 (2017)","journal-title":"J. Autom. Reasoning"},{"key":"29_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-26529-2_5","volume-title":"Programming Languages and Systems","author":"M Tatsuta","year":"2015","unstructured":"Tatsuta, M., Kimura, D.: Separation logic with monadic inductive definitions and implicit existentials. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 69\u201389. Springer, Cham (2015). doi: 10.1007\/978-3-319-26529-2_5"},{"key":"29_CR39","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.W.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 402\u2013416. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45931-6_28"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,29]],"date-time":"2019-09-29T04:28:54Z","timestamp":1569731334000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}