{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T02:48:18Z","timestamp":1777949298302,"version":"3.51.4"},"publisher-location":"Singapore","reference-count":41,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819578252","type":"print"},{"value":"9789819578269","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-7826-9_8","type":"book-chapter","created":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T22:40:43Z","timestamp":1777848043000},"page":"134-153","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Separation Logic with\u00a0Heap Variables: A Decision Procedure and\u00a0Its Application"],"prefix":"10.1007","author":[{"given":"Xie","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yutian","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,1]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"8_CR3","unstructured":"Beyer, D.: Memory-safety track of SV-COMP 2024 benchmarks. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks\/-\/tree\/main\/c\/mem-safety"},{"key":"8_CR4","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Proceedings of the 2nd IFIP Congress on Information Processing, pp. 21\u201328 (1962)"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/322169.322185","volume":"27","author":"N Suzuki","year":"1980","unstructured":"Suzuki, N., Jefferson, D.: Verification decidability of Presburger array programs. J. ACM 27(1), 191\u2013205 (1980)","journal-title":"J. ACM"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"JR Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68\u201380. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_44"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-54108-7_6","volume-title":"Verified Software: Theories, Tools, Experiments","author":"S Falke","year":"2014","unstructured":"Falke, S., Merz, F., Sinz, C.: Extending the theory of arrays: memset, memcpy, and beyond. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 108\u2013128. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_6"},{"key":"8_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). https:\/\/doi.org\/10.1007\/11609773_28"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Gadelha, M.Y.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength C model checker. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, pp. 888\u2013891 (2018)","DOI":"10.1145\/3238147.3240481"},{"issue":"3","key":"8_CR11","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/3242953.3242964","volume":"5","author":"C Haase","year":"2018","unstructured":"Haase, C.: A survival guide to Presburger arithmetic. ACM SIGLOG News 5(3), 67\u201382 (2018)","journal-title":"ACM SIGLOG News"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-030-68446-4_9","volume-title":"Logic-Based Program Synthesis and Transformation","author":"Z Esen","year":"2021","unstructured":"Esen, Z., R\u00fcmmer, P.: Reasoning in the theory of heap: satisfiability and interpolation. In: LOPSTR 2020. LNCS, vol. 12561, pp. 173\u2013191. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_9"},{"key":"8_CR13","unstructured":"Esen, Z., R\u00fcmmer, P.: An SMT-LIB theory of heaps. In: Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories. Volume 3185 of CEUR Workshop Proceedings, pp. 38\u201353 (2022)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Vafeiadis, V., Berdine, J.: Structuring the verification of heap-manipulating programs. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 261\u2013274. ACM (2010)","DOI":"10.1145\/1706299.1706331"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-662-46669-8_26","volume-title":"Programming Languages and Systems","author":"A Albargouthi","year":"2015","unstructured":"Albargouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 634\u2013660. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_26"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-319-52234-0_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Hol\u00edk","year":"2017","unstructured":"Hol\u00edk, L., Hru\u0161ka, M., Leng\u00e1l, O., Rogalewicz, A., Vojnar, T.: Counterexample validation and interpolation-based refinement for forest automata. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 288\u2013309. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_16"},{"key":"8_CR17","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 2011, pp. 235\u2013249 (2011)","DOI":"10.1007\/978-3-642-23217-6_16"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Fuhs, C., Perez, J.A.N., Gorogiannis, N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: LICS 2014, pp. 25:1\u201325:10 (2014)","DOI":"10.1145\/2603088.2603091"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575467_5"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Hou, Z., Gor\u00e9, R., Tiu, A.: Automated theorem proving for assertions in separation logic with all connectives. In: CADE 2015, pp. 501\u2013516 (2015)","DOI":"10.1007\/978-3-319-21401-6_34"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M.I., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: FoSSaCS 2014, pp. 411\u2013425 (2014)","DOI":"10.1007\/978-3-642-54830-7_27"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Enea, C., Lengal, O., Sighireanu, M., Vojnar, T.: Compositional entailment checking for a fragment of separation logic. Technical report FIT-TR-2014-01, FIT, Brno University of Technology. APLAS 2014 (2014)","DOI":"10.1007\/978-3-319-12736-1_17"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: CADE 2013, pp. 21\u201338 (2013)","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding entailments in inductive separation logic with tree automata. In: ATVA 2014, pp. 201\u2013218 (2014)","DOI":"10.1007\/978-3-319-11936-6_15"},{"key":"8_CR25","unstructured":"Chen, T., Song, F., Wu, Z.: Tractability of separation logic with inductive definitions: beyond lists. In: Proceedings of the 28th International Conference on Concurrency Theory. Volume 85 of LIPIcs, pp. 37:1\u201337:17 (2017)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Gorogiannis, N., Kanovich, M.I., Rowe, R.: Model checking for symbolic-heap separation logic with inductive predicates. In: POPL 2016, pp. 84\u201396 (2016)","DOI":"10.1145\/2837614.2837621"},{"key":"8_CR27","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":"8_CR28","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, pp. 244\u2013261 (2016)","DOI":"10.1007\/978-3-319-46520-3_16"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-52234-0_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Iosif, R., Serban, C.: Reasoning in the Bernays-Sch\u00f6nfinkel-Ramsey fragment of separation logic. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 462\u2013482. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_25"},{"key":"8_CR30","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, \u00c9.: On the almighty wand. Inf. Comput. 211, 106\u2013137 (2012)","journal-title":"Inf. Comput."},{"issue":"9","key":"8_CR31","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W Chin","year":"2012","unstructured":"Chin, W., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"8_CR32","first-page":"532","volume":"2016","author":"X Gu","year":"2016","unstructured":"Gu, X., Chen, T., Wu, Z.: A complete decision procedure for linearly compositional separation logic with data constraints. IJCAR 2016, 532\u2013549 (2016)","journal-title":"IJCAR"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Tatsuta, M., Le, Q.L., Chin, W.: Decision procedure for separation logic with inductive definitions and Presburger arithmetic. In: APLAS 2016, pp. 423\u2013443 (2016)","DOI":"10.1007\/978-3-319-47958-3_22"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Le, Q.L., Sun, J., Chin, W.: Satisfiability modulo heap-based programs. In: CAV 2016, pp. 382\u2013404 (2016)","DOI":"10.1007\/978-3-319-41528-4_21"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: ATVA 2016, pp. 244\u2013261 (2016)","DOI":"10.1007\/978-3-319-46520-3_16"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Xu, Z., Chen, T., Wu, Z.: Satisfiability of compositional separation logic with tree predicates and data constraints. Technical report, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (2017)","DOI":"10.1007\/978-3-319-63046-5_31"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-030-10801-4_17","volume-title":"SOFSEM 2019: Theory and Practice of Computer Science","author":"C Gao","year":"2019","unstructured":"Gao, C., Chen, T., Wu, Z.: Separation logic with linearly compositional inductive predicates and set data constraints. In: Catania, B., Kr\u00e1lovi\u010d, R., Nawrocki, J., Pighizzini, G. (eds.) SOFSEM 2019. LNCS, vol. 11376, pp. 206\u2013220. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-10801-4_17"},{"key":"8_CR38","unstructured":"Priya, S., Su, Y., Bao, Y., Zhou, X., Vizel, Y., Gurfinkel, A.: Bounded model checking for LLVM. In: Proceedings of the 22nd Formal Methods in Computer-Aided Design, pp. 214\u2013224 (2022)"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F Merz","year":"2012","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146\u2013161. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_12"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"8_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-7826-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T22:40:45Z","timestamp":1777848045000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-7826-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9789819578252","9789819578269"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-7826-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"1 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 December 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.setta2025.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}