{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:50:41Z","timestamp":1743004241987,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319631387"},{"type":"electronic","value":"9783319631394"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63139-4_9","type":"book-chapter","created":{"date-parts":[[2017,7,23]],"date-time":"2017-07-23T23:22:55Z","timestamp":1500852175000},"page":"151-167","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators"],"prefix":"10.1007","author":[{"given":"Bin","family":"Fang","sequence":"first","affiliation":[]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,25]]},"reference":[{"key":"9_CR1","unstructured":"Aldridge, L.: Memory allocation in C. In: Embedded Systems Programming, pp. 35\u201342, August 2008"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11823230_15","volume-title":"Static Analysis","author":"G Balakrishnan","year":"2006","unstructured":"Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221\u2013239. Springer, Heidelberg (2006). doi:\n                      10.1007\/11823230_15"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Dragoi, C., Enea, C., Sighireanu, M.: On inter-procedural analysis of programs with lists and data. In: PLDI, pp. 578\u2013589. ACM (2011)","DOI":"10.1145\/1993316.1993566"},{"key":"9_CR4","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:\n                      10.1007\/978-3-642-33386-6_14"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11823230_13","volume-title":"Static Analysis","author":"C Calcagno","year":"2006","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Beyond reachability: shape abstraction in the presence of pointer arithmetic. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 182\u2013203. Springer, Heidelberg (2006). doi:\n                      10.1007\/11823230_13"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Chang, B.E., Rival, X.: Modular construction of shape-numeric analyzers. In: Semantics, Abstract Interpretation, and Reasoning about Programs, EPTCS, vol. 129, pp. 161\u2013185 (2013)","DOI":"10.4204\/EPTCS.129.11"},{"key":"9_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: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384\u2013401. Springer, Heidelberg (2007). doi:\n                      10.1007\/978-3-540-74061-2_24"},{"key":"9_CR8","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: POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"9_CR9","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). doi:\n                      10.1007\/11691372_19"},{"key":"9_CR10","unstructured":"Dragoi, C.: Automated verification of heap-manipulating programs with infinite data. PhD thesis, University Paris Diderot (2011)"},{"key":"9_CR11","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). doi:\n                      10.1007\/978-3-642-38856-9_10"},{"key":"9_CR12","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:\n                      10.1007\/978-3-319-24953-7_7"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, S.: A combination framework for tracking partition sizes. In: POPL, pp. 239\u2013251. ACM (2009)","DOI":"10.1145\/1594834.1480912"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235\u2013246. ACM (2008)","DOI":"10.1145\/1328897.1328468"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: PLDI, pp. 339\u2013348. ACM (2008)","DOI":"10.1145\/1379022.1375623"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). doi:\n                      10.1007\/978-3-642-02658-4_52"},{"key":"9_CR17","volume-title":"The C Programming Language","author":"BW Kernighan","year":"1988","unstructured":"Kernighan, B.W., Ritchie, D.: The C Programming Language, 2nd edn. Prentice-Hall, Englewood Cliffs (1988)","edition":"2"},{"issue":"3","key":"9_CR18","first-page":"573","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. FAC 27(3), 573\u2013609 (2015)","journal-title":"FAC"},{"key":"9_CR19","volume-title":"The Art of Computer Programming, Volume I: Fundamental Algorithms","author":"DE Knuth","year":"1973","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume I: Fundamental Algorithms, 2nd edn. Addison-Wesley, Reading (1973)","edition":"2"},{"key":"9_CR20","unstructured":"Lea, D.: dlmalloc (2012). \n                      ftp:\/\/gee.cs.oswego.edu\/pub\/misc\/malloc.c"},{"key":"9_CR21","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). doi:\n                      10.1007\/978-3-642-22110-1_48"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-662-46081-8_16","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). doi:\n                      10.1007\/978-3-662-46081-8_16"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-05089-3_24","volume-title":"FM 2009: Formal Methods","author":"E Albert","year":"2009","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Field-sensitive value analysis by field-insensitive analysis. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 370\u2013386. Springer, Heidelberg (2009). doi:\n                      10.1007\/978-3-642-05089-3_24"},{"key":"9_CR24","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:\n                      10.1007\/3-540-44802-0_1"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-35182-2_10","volume-title":"Programming Languages and Systems","author":"P Sotin","year":"2012","unstructured":"Sotin, P., Rival, X.: Hierarchical shape abstraction of dynamic structures in static blocks. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 131\u2013147. Springer, Heidelberg (2012). doi:\n                      10.1007\/978-3-642-35182-2_10"},{"key":"9_CR26","unstructured":"Celia extensions. \n                      http:\/\/www.irif.fr\/~sighirea\/celia\/plus.html"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-60368-9_19","volume-title":"Memory Management","author":"PR Wilson","year":"1995","unstructured":"Wilson, P.R., Johnstone, M.S., Neely, M., Boles, D.: Dynamic storage allocation: a survey and critical review. In: Baler, H.G. (ed.) IWMM 1995. LNCS, vol. 986, pp. 1\u2013116. Springer, Heidelberg (1995). doi:\n                      10.1007\/3-540-60368-9_19"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63139-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:51:48Z","timestamp":1558320708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63139-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631387","9783319631394"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63139-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"25 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Edinburgh","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":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 September 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.cliplab.org\/Conferences\/LOPSTR16\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}