{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:34:49Z","timestamp":1770273289365,"version":"3.49.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633893","type":"print"},{"value":"9783319633909","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_26","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"495-517","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["A Decidable Fragment in Separation Logic with\u00a0Inductive Predicates and Arithmetic"],"prefix":"10.1007","author":[{"given":"Quang Loc","family":"Le","sequence":"first","affiliation":[]},{"given":"Makoto","family":"Tatsuta","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"26_CR1","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":"26_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":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403\u2013418. Springer, Heidelberg (2000). doi:10.1007\/10722167_31"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14295-6_23","volume-title":"Computer Aided Verification","author":"M Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227\u2013242. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14295-6_23"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Fuhs, C., P\u00e9rez, J.A.N., Gorogiannis, N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: CSL-LICS 2014, pp. 25:1\u201325:10, (2014). ACM, New York","DOI":"10.1145\/2603088.2603091"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-319-10936-7_5","volume-title":"Static Analysis","author":"J Brotherston","year":"2014","unstructured":"Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 68\u201384. Springer, Cham (2014). doi:10.1007\/978-3-319-10936-7_5"},{"key":"26_CR7","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). doi:10.1007\/3-540-45294-X_10"},{"issue":"9","key":"26_CR8","first-page":"1006","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. SCP 77(9), 1006\u20131036 (2012)","journal-title":"SCP"},{"key":"26_CR9","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":"26_CR10","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). doi:10.1007\/978-3-540-78800-3_24"},{"key":"26_CR11","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":"26_CR12","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). doi:10.1007\/978-3-319-40229-1_36"},{"key":"26_CR13","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). doi:10.1007\/978-3-642-38574-2_2"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM POPL, pp. 14\u201326, London, January 2001","DOI":"10.1145\/373243.375719"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-08867-9_4","volume-title":"Computer Aided Verification","author":"QL Le","year":"2014","unstructured":"Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52\u201368. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_4"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-38088-4_20","volume-title":"NASA Formal Methods","author":"QL Le","year":"2013","unstructured":"Le, Q.L., Sharma, A., Craciun, F., Chin, W.-N.: Towards complete specifications with an error calculus. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 291\u2013306. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-38088-4_20"},{"key":"26_CR17","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":"26_CR18","unstructured":"Le, Q.L., Sun, J., Qin, S.: Verifying heap-manipulating programs using constrained horn clauses (technical report) (2017)"},{"key":"26_CR19","unstructured":"Le, Q.L., Sun, J., Qin, S., Chin, W.-N.: Frame inference for inductive entailment proofs in separation logic (technical report), May 2016"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Le, Q.L., Tatsuta, M., Jun, S., Chin, W.-N.: A decidable fragment in separation logic with inductive predicates and arithmetic (technical report) (2017)","DOI":"10.1007\/978-3-319-63390-9_26"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI 2011, pp. 556\u2013566. ACM (2011)","DOI":"10.1145\/1993316.1993563"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-319-03542-0_7","volume-title":"Programming Languages and Systems","author":"JA Navarro P\u00e9rez","year":"2013","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic modulo theories. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 90\u2013106. Springer, Cham (2013). doi:10.1007\/978-3-319-03542-0_7"},{"key":"26_CR23","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":"26_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-54862-8_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: GRASShopper: complete heap verification with mixed specifications. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 124\u2013139. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54862-8_9"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-77505-8_26","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"C Popeea","year":"2007","unstructured":"Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331\u2013345. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-77505-8_26"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Qiu, X., Garg, P., \u015etef\u0103nescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI, pp. 231\u2013242 (2013). ACM, New York","DOI":"10.1145\/2499370.2462169"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: IEEE LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"26_CR28","unstructured":"Serban, C.: A formalization of separation logic in SMT-LIB v2.5 syntax, types and semantics. Technical report, Verimag (2015) Accessed Jan 2017"},{"key":"26_CR29","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":"26_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-319-03542-0_8","volume-title":"Programming Languages and Systems","author":"M-T Trinh","year":"2013","unstructured":"Trinh, M.-T., Le, Q.L., David, C., Chin, W.-N.: Bi-abduction with pure properties for specification inference. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 107\u2013123. Springer, Cham (2013). doi:10.1007\/978-3-319-03542-0_8"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:10:28Z","timestamp":1750554628000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}