{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:58:52Z","timestamp":1779087532187,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642157684","type":"print"},{"value":"9783642157691","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15769-1_6","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T06:09:40Z","timestamp":1284358180000},"page":"71-99","source":"Crossref","is-referenced-by-count":17,"title":["Statically Inferring Complex Heap, Array, and Numeric Invariants"],"prefix":"10.1007","author":[{"given":"Bill","family":"McCloskey","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/11823230_14","volume-title":"Static Analysis","author":"G. Arnold","year":"2006","unstructured":"Arnold, G.: Specialized 3-valued logic shape analysis using structure-based refinement and loose embedding. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 204\u2013220. Springer, Heidelberg (2006)"},{"key":"6_CR2","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., 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":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 517\u2013531. Springer, Heidelberg (2006)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-78800-3_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2008","unstructured":"Clarke, E., Talupur, M., Veith, H.: Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 33\u201347. Springer, Heidelberg (2008)"},{"issue":"1-3","key":"6_CR5","first-page":"27","volume":"38","author":"A. Cortesi","year":"2000","unstructured":"Cortesi, A., Charlier, B.L., Hentenryck, P.V.: Combinations of abstract domains for logic programming. SCP\u00a038(1-3), 27\u201371 (2000)","journal-title":"SCP"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"6_CR7","unstructured":"DeLine, R., Leino, K.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Deutsch, A.: Interprocedural alias analysis for pointers: Beyond k-limiting. In: PLDI, pp. 230\u2013241 (1994)","DOI":"10.1145\/773473.178263"},{"key":"6_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., 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":"6_CR10","doi-asserted-by":"crossref","unstructured":"Dor, N., Rodeh, M., Sagiv, M.: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: PLDI, pp. 155\u2013167 (2003)","DOI":"10.1145\/781131.781149"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Emmi, M., Jhala, R., Kohler, E., Majumdar, R.: Verifying reference counting implementations. In: TACAS (2009)","DOI":"10.1007\/978-3-642-00768-2_30"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-24730-2_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Gopan","year":"2004","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 512\u2013529. Springer, Heidelberg (2004)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"P. Granger","year":"1992","unstructured":"Granger, P.: Improving the results of static analyses programs by local decreasing iteration. In: Shyamasundar, R.K. (ed.) FSTTCS 1992. LNCS, vol.\u00a0652, Springer, Heidelberg (1992)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: POPL, pp. 239\u2013251 (2009)","DOI":"10.1145\/1594834.1480912"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI (2006)","DOI":"10.1145\/1133981.1134026"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/11547662_14","volume-title":"Static Analysis","author":"B. Jeannet","year":"2005","unstructured":"Jeannet, B., Gopan, D., Reps, T.: A relational abstraction for functions. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 186\u2013202. Springer, Heidelberg (2005)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-540-74061-2_26","volume-title":"Static Analysis","author":"S. Magill","year":"2007","unstructured":"Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic strengthening for shape analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 419\u2013436. Springer, Heidelberg (2007)"},{"key":"6_CR18","unstructured":"McCloskey, B.: Deskcheck 1.0, http:\/\/www.cs.berkeley.edu\/~billm\/deskcheck"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol.\u00a02053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"issue":"2","key":"6_CR20","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"TOPLAS"},{"key":"6_CR21","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":"H. Nguyen","year":"2007","unstructured":"Nguyen, H., David, C., Qin, S., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 251\u2013266. Springer, Heidelberg (2007)"},{"key":"6_CR22","unstructured":"Poskanzer, J.: thttpd - tiny\/turbo\/throttling http server, http:\/\/acme.com\/software\/thttpd\/"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"issue":"3","key":"6_CR24","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. TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"TOPLAS"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: ACM Conf. Programming Language Design and Implementation, PLDI (2008)","DOI":"10.1145\/1375581.1375624"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: An integrated proof language for imperative programs. In: PLDI, pp. 338\u2013351 (2009)","DOI":"10.1145\/1542476.1542514"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15769-1_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:40:20Z","timestamp":1606185620000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15769-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642157684","9783642157691"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15769-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}