{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:20:00Z","timestamp":1770272400102,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662482872","type":"print"},{"value":"9783662482889","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-662-48288-9_6","type":"book-chapter","created":{"date-parts":[[2015,9,1]],"date-time":"2015-09-01T02:26:24Z","timestamp":1441074384000},"page":"90-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Shape Analysis for Unstructured Sharing"],"prefix":"10.1007","author":[{"given":"Huisong","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bor-Yuh Evan","family":"Chang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,9,2]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"6_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)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-27940-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Abstract domains for automated reasoning about list-manipulating programs with infinite data. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 1\u201322. Springer, Heidelberg (2012)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Symposium on Principles of Programming Languages (POPL), pp. 289\u2013300. ACM (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: Symposium on Principles of Programming Languages (POPL), pp. 247\u2013260. ACM (2008)","DOI":"10.1145\/1328897.1328469"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Modular construction of shape-numeric analyzers. In: Festschrift for Dave Schmidt. ENTCS, pp. 161\u2013185 (2013)","DOI":"10.4204\/EPTCS.129.11"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-74061-2_24","volume-title":"Static Analysis","author":"B-YE Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384\u2013401. Springer, Heidelberg (2007)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-15769-1_13","volume-title":"Static Analysis","author":"R Cherini","year":"2010","unstructured":"Cherini, R., Rearte, L., Blanco, J.: A shape analysis for non-linear data structures. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 201\u2013217. Springer, Heidelberg (2010)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symposium on Principles of Programming Languages (POPL) (1977)","DOI":"10.1145\/512950.512973"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Symposium on Principles of Programming Languages (POPL) (1979)","DOI":"10.1145\/567752.567778"},{"key":"6_CR11","unstructured":"Cox, A.: Binary-Decision-Diagrams for Set Abstraction. ArXiv e-prints, March 2015"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-319-10936-7_9","volume-title":"Static Analysis","author":"A Cox","year":"2014","unstructured":"Cox, A., Chang, B.-Y.E., Rival, X.: Automatic analysis of open objects in dynamic language programs. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 134\u2013150. Springer, Heidelberg (2014)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: Symposium on Principles of Programming Languages (POPL), pp. 187\u2013200. ACM (2011)","DOI":"10.1145\/1925844.1926407"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-38856-9_10","volume-title":"Static Analysis","author":"C Dr\u0103goi","year":"2013","unstructured":"Dr\u0103goi, C., Enea, C., Sighireanu, M.: Local shape analysis for overlaid data structures. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 150\u2013171. Springer, Heidelberg (2013)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-33826-7_5","volume-title":"Software Engineering and Formal Methods","author":"P Ferrara","year":"2012","unstructured":"Ferrara, P., Fuchs, R., Juhasz, U.: TVAL+ : TVLA and value analyses together. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 63\u201377. Springer, Heidelberg (2012)"},{"key":"6_CR17","unstructured":"Filliatre, J.-C.: Bdd ocaml library. https:\/\/www.lri.fr\/filliatr\/ftp\/ocaml\/bdd\/"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: Symposium on Principles of Programming Languages (POPL), pp. 14\u201326. ACM (2001)","DOI":"10.1145\/373243.375719"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-11319-2_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Kreiker","year":"2010","unstructured":"Kreiker, J., Seidl, H., Vojdani, V.: Shape analysis of low-level C with overlapping structures. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 214\u2013230. Springer, Heidelberg (2010)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-22110-1_48","volume-title":"Computer Aided Verification","author":"O Lee","year":"2011","unstructured":"Lee, O., Yang, H., Petersen, R.: Program Analysis for Overlaid Data Structures. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 592\u2013608. Springer, Heidelberg (2011)"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: a system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280\u2013302. Springer, Heidelberg (2000)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","first-page":"282","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Liu","year":"2015","unstructured":"Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 282\u2013299. Springer, Heidelberg (2015)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"HH Nguyen","year":"2007","unstructured":"Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251\u2013266. Springer, Heidelberg (2007)"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Symposium on Logics In Computer Science (LICS), pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"6_CR25","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. (TOPLAS) 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-35873-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Toubhans","year":"2013","unstructured":"Toubhans, A., Chang, B.-Y.E., Rival, X.: Reduced Product Combination of Abstract Domains for Shapes. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 375\u2013395. Springer, Heidelberg (2013)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/978-3-319-10936-7_18","volume-title":"Static Analysis","author":"A Toubhans","year":"2014","unstructured":"Toubhans, A., Chang, B.-Y.E., Rival, X.: An abstract domain combinator for separately conjoining memory abstractions. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 285\u2013301. Springer, Heidelberg (2014)"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-540-93900-9_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V Vafeiadis","year":"2009","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 335\u2013348. Springer, Heidelberg (2009)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-61739-6_53","volume-title":"Static Analysis","author":"A Venet","year":"1996","unstructured":"Venet, A.: Abstract cofibered domains: application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 366\u2013382. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48288-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T09:57:55Z","timestamp":1748599075000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-48288-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662482872","9783662482889"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48288-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"2 September 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}