{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:37:33Z","timestamp":1759639053351},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"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_31","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"509-527","source":"Crossref","is-referenced-by-count":6,"title":["Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints"],"prefix":"10.1007","author":[{"given":"Zhaowei","family":"Xu","sequence":"first","affiliation":[]},{"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-319-02444-8_17","volume-title":"Automated Technology for Verification and Analysis","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Hol\u00edk, L., Jonsson, B., Leng\u00e1l, O., Trinh, C.Q., Vojnar, T.: Verification of heap manipulating programs with ordered data by extended forest automata. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 224\u2013239. Springer, Cham (2013). doi: 10.1007\/978-3-319-02444-8_17"},{"key":"31_CR2","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). doi: 10.1007\/11575467_5"},{"key":"31_CR3","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":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR \u201997: Concurrency Theory","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135\u2013150. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63141-0_10"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-22438-6_12","volume-title":"Automated Deduction \u2013 CADE-23","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 131\u2013146. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_12"},{"key":"31_CR6","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, pp. 25:1\u201325:10 (2014)","DOI":"10.1145\/2603088.2603091"},{"issue":"1","key":"31_CR7","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (1981)","journal-title":"J. ACM"},{"issue":"9","key":"31_CR8","doi-asserted-by":"crossref","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W-N 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. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Chu, D.-H., Jaffar, J., Trinh, M.-T.: Automatic induction proofs of data-structures in imperative programs. In: PLDI, pp. 457\u2013466 (2015)","DOI":"10.1145\/2737924.2737984"},{"issue":"2","key":"31_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-4(2:8)2008","volume":"4","author":"H Comon-Lundh","year":"2008","unstructured":"Comon-Lundh, H., Jacquemard, F., Perrin, N.: Visibly tree automata with memory and constraints. Logical Methods Comput. Sci. 4(2), 1\u201336 (2008)","journal-title":"Logical Methods Comput. Sci."},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Creus, C., Godoy, G.: Tree automata with height constraints between brothers. In: RTA-TLCA, pp. 149\u2013163 (2014)","DOI":"10.1007\/978-3-319-08918-8_11"},{"key":"31_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-319-12736-1_17","volume-title":"Programming Languages and Systems","author":"C Enea","year":"2014","unstructured":"Enea, C., Leng\u00e1l, O., Sighireanu, M., Vojnar, T.: Compositional entailment checking for a fragment of separation logic. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 314\u2013333. Springer, Cham (2014). doi: 10.1007\/978-3-319-12736-1_17"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-319-24953-7_7","volume-title":"Automated Technology for Verification and Analysis","author":"C Enea","year":"2015","unstructured":"Enea, C., Sighireanu, M., Wu, Z.: On automated lemma generation for separation logic with inductive definitions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 80\u201396. Springer, Cham (2015). doi: 10.1007\/978-3-319-24953-7_7"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Gu, X., Chen, T., Wu, Z.: A complete decision procedure for linearly compositional separation logic with data constraints. In: IJCAR, pp. 532\u2013549 (2016)","DOI":"10.1007\/978-3-319-40229-1_36"},{"key":"31_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-04081-8_25","volume-title":"CONCUR 2009 - Concurrency Theory","author":"C Haase","year":"2009","unstructured":"Haase, C., Kreutzer, S., Ouaknine, J., Worrell, J.: Reachability in succinct and parametric one-counter automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 369\u2013383. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04081-8_25"},{"issue":"1","key":"31_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s00236-009-0108-5","volume":"47","author":"P Habermehl","year":"2010","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: Automata-based verification of programs with tree updates. Acta Inf. 47(1), 1\u201331 (2010)","journal-title":"Acta Inf."},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-319-21401-6_34","volume-title":"Automated Deduction - CADE-25","author":"Z H\u00f3u","year":"2015","unstructured":"H\u00f3u, Z., Gor\u00e9, R., Tiu, A.: Automated theorem proving for assertions in separation logic with all connectives. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 501\u2013516. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_34"},{"key":"31_CR18","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":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-11936-6_15","volume-title":"Automated Technology for Verification and Analysis","author":"R Iosif","year":"2014","unstructured":"Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding entailments in inductive separation logic with tree automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 201\u2013218. Springer, Cham (2014). doi: 10.1007\/978-3-319-11936-6_15"},{"key":"31_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). doi: 10.1007\/978-3-319-41528-4_21"},{"key":"31_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-72734-7_26","volume-title":"Logical Foundations of Computer Science","author":"Z Manna","year":"2007","unstructured":"Manna, Z., Sipma, H.B., Zhang, T.: Verifying balanced trees. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 363\u2013378. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-72734-7_26"},{"key":"31_CR22","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). doi: 10.1007\/3-540-44802-0_1"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in C using separation logic. In: PLDI, pp. 440\u2013451 (2014)","DOI":"10.1145\/2666356.2594325"},{"key":"31_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2013","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773\u2013789. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_54"},{"key":"31_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/978-3-319-08867-9_47","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711\u2013728. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_47"},{"key":"31_CR26","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: GRASShopper - complete heap verification with mixed specifications. In: TACAS, pp. 124\u2013139 (2014)","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"31_CR27","doi-asserted-by":"crossref","unstructured":"Qiu, X., Garg, P., Stef\u0103nescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI, pp. 231\u2013242 (2013)","DOI":"10.1145\/2499370.2462169"},{"issue":"1","key":"31_CR28","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(93)90222-F","volume":"116","author":"PZ Revesz","year":"1993","unstructured":"Revesz, P.Z.: A closed-form evaluation for datalog queries with integer (gap)-order constraints. Theor. Comput. Sci. 116(1), 117\u2013149 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"31_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-319-46520-3_16","volume-title":"Automated Technology for Verification and Analysis","author":"A Reynolds","year":"2016","unstructured":"Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 244\u2013261. Springer, Cham (2016). doi: 10.1007\/978-3-319-46520-3_16"},{"key":"31_CR30","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"31_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347\u2013363. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_24"},{"key":"31_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1136","DOI":"10.1007\/978-3-540-27836-8_94","volume-title":"Automata, Languages and Programming","author":"H Seidl","year":"2004","unstructured":"Seidl, H., Schwentick, T., Muscholl, A., Habermehl, P.: Counting in trees for free. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1136\u20131149. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27836-8_94"},{"key":"31_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-319-47958-3_22","volume-title":"Programming Languages and Systems","author":"M Tatsuta","year":"2016","unstructured":"Tatsuta, M., Le, Q.L., Chin, W.-N.: Decision procedure for separation logic with inductive definitions and presburger arithmetic. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 423\u2013443. Springer, Cham (2016). doi: 10.1007\/978-3-319-47958-3_22"},{"key":"31_CR34","unstructured":"Z3. http:\/\/rise4fun.com\/z3"}],"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_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,29]],"date-time":"2019-09-29T08:28:56Z","timestamp":1569745736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}