{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:26:08Z","timestamp":1770283568119,"version":"3.49.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319088662","type":"print"},{"value":"9783319088679","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08867-9_4","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T11:37:30Z","timestamp":1403955450000},"page":"52-68","source":"Crossref","is-referenced-by-count":37,"title":["Shape Analysis via Second-Order Bi-Abduction"],"prefix":"10.1007","author":[{"given":"Quang Loc","family":"Le","sequence":"first","affiliation":[]},{"given":"Cristian","family":"Gherghina","sequence":"additional","affiliation":[]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Glib-2.38.2 (2013), https:\/\/developer.gnome.org\/glib\/ (accessed November 13, 2013)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Alpuente, M., Feli\u00fa, M.A., Villanueva, A.: Automatic inference of specifications using matching logic. In: PEPM, pp. 127\u2013136 (2013)","DOI":"10.1145\/2426890.2426914"},{"key":"4_CR3","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.\u00a04590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"4_CR4","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.\u00a06806, pp. 178\u2013183. Springer, Heidelberg (2011)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. Technical Report RN\/13\/14, University College London (2013)","DOI":"10.1007\/978-3-319-10936-7_5"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL, pp. 289\u2013300 (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-642-10672-9_19","volume-title":"Programming Languages and Systems","author":"C. Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., Vafeiadis, V.: Bi-abductive resource invariant synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 259\u2013274. Springer, Heidelberg (2009)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: POPL, pp. 247\u2013260 (2008)","DOI":"10.1145\/1328897.1328469"},{"issue":"9","key":"4_CR9","doi-asserted-by":"publisher","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.\u00a077(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A., Sagiv, M.: Precise and compact modular procedure summaries for heap manipulating programs. In: PLDI, pp. 567\u2013577 (2011)","DOI":"10.1145\/1993316.1993565"},{"key":"4_CR11","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.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-22110-1_29","volume-title":"Computer Aided Verification","author":"K. Dudka","year":"2011","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: A practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 372\u2013378. Springer, Heidelberg (2011)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/11823230_16","volume-title":"Static Analysis","author":"A. Gotsman","year":"2006","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Interprocedural Shape Analysis with Separated Heap Abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 240\u2013260. Springer, Heidelberg (2006)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416 (2012)","DOI":"10.1145\/2345156.2254112"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-03237-0_14","volume-title":"Static Analysis","author":"B.S. Gulavani","year":"2009","unstructured":"Gulavani, B.S., Chakraborty, S., Ramalingam, G., Nori, A.V.: Bottom-up shape analysis. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 188\u2013204. Springer, Heidelberg (2009)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: PLDI, pp. 256\u2013265 (2007)","DOI":"10.1145\/1273442.1250764"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-41202-8_26","volume-title":"Formal Methods and Software Engineering","author":"G. He","year":"2013","unstructured":"He, G., Qin, S., Chin, W.-N., Craciun, F.: Automated specification discovery via user-defined predicates. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol.\u00a08144, pp. 397\u2013414. Springer, Heidelberg (2013)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"740","DOI":"10.1007\/978-3-642-39799-8_52","volume-title":"Computer Aided Verification","author":"L. Hol\u00edk","year":"2013","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 740\u2013755. Springer, Heidelberg (2013)"},{"key":"4_CR19","series-title":"LNAI","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.\u00a07898, pp. 21\u201338. Springer, Heidelberg (2013)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an Assertion Language for Mutable Data Structures. In: ACM POPL, London (January 2001)","DOI":"10.1145\/360204.375719"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Le, Q.L., Gherghina, C., Qin, S., Chin, W.N.: Shape analysis via second-order bi-abduction. In Technical Report, Soc, NUS (February 2014), http:\/\/loris-7.ddns.comp.nus.edu.sg\/~project\/s2\/beta\/src\/TRs2.pdf","DOI":"10.1007\/978-3-319-08867-9_4"},{"key":"4_CR22","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.\u00a06806, pp. 592\u2013608. Springer, Heidelberg (2011)"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-31987-0_10","volume-title":"Programming Languages and Systems","author":"O. Lee","year":"2005","unstructured":"Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 124\u2013140. Springer, Heidelberg (2005)"},{"key":"4_CR24","unstructured":"Lev-Ami, T., Sagiv, M., Reps, T., Gulwani, S.: Backward analysis for inferring quantified preconditions. Technical Report TR-2007-12-01, Tel Aviv University (2007)"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/11513988_50","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Abstraction Refinement via Inductive Learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 519\u2013533. Springer, Heidelberg (2005)"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: Automatic numeric abstractions for heap-manipulating programs. In: POPL, pp. 211\u2013222 (2010)","DOI":"10.1145\/1707801.1706326"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G. Necula","year":"2002","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"4_CR28","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":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/11547662_20","volume-title":"Static Analysis","author":"N. Rinetzky","year":"2005","unstructured":"Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural\u00a0shape\u00a0analysis for\u00a0cutpoint-free\u00a0programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 284\u2013302. Springer, Heidelberg (2005)"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Rival, X., Chang, B.-Y.E.: Calling context abstraction with shapes. In: POPL, pp. 173\u2013186 (2011)","DOI":"10.1145\/1925844.1926406"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Rosu, G., Stefanescu, A.: Checking reachability using matching logic. In: OOPSLA, pp. 555\u2013574. ACM (2012)","DOI":"10.1145\/2398857.2384656"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08867-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T14:01:54Z","timestamp":1746280914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08867-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319088662","9783319088679"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08867-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}