{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:58:03Z","timestamp":1725569883465},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_13","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T12:40:06Z","timestamp":1289220006000},"page":"171-187","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Heap-Manipulating Programs with Unknown Procedure Calls"],"prefix":"10.1007","author":[{"given":"Shengchao","family":"Qin","sequence":"first","affiliation":[]},{"given":"Chenguang","family":"Luo","sequence":"additional","affiliation":[]},{"given":"Guanhua","family":"He","sequence":"additional","affiliation":[]},{"given":"Florin","family":"Craciun","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Ammons, G., Bodik, R., Larus, J.R.: Mining specifications. In: POPL (2002)","DOI":"10.1145\/503272.503275"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Beizer, B., Wiley, J.: Black-box testing: techniques for functional testing of software and systems. IEEE Software\u00a013(5) (September 1996)","DOI":"10.1109\/MS.1996.536464"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: 36th POPL (January 2009)","DOI":"10.1145\/1480881.1480917"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Emami, M., Ghiya, R., Hendren, L.J.: Context-sensitive interprocedural points-to analysis in the presence of function pointers. In: PLDI (1994)","DOI":"10.1145\/178243.178264"},{"key":"13_CR5","unstructured":"Giacobazzi, R.: Abductive analysis of modular logic programs. In: ILPS (1994)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-73368-3_10","volume-title":"Computer Aided Verification","author":"D. Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Low-level library analysis and summarization. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 68\u201381. Springer, Heidelberg (2007)"},{"issue":"5","key":"13_CR7","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/MS.1998.714621","volume":"15","author":"W. Kozaczynski","year":"1998","unstructured":"Kozaczynski, W., Booch, G.: Component-based software engineering. IEEE Software\u00a015(5), 34\u201336 (1998)","journal-title":"IEEE Software"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Luo, C., Craciun, F., Qin, S., He, G., Chin, W.-N.: Verifying pointer safety for programs with unknown calls. Journal of Symbolic Computation (to appear)","DOI":"10.1016\/j.jsc.2010.06.003"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Qin, S., Luo, C., He, G., Craciun, F., Chin, W.-N.: Verifying heap-manipulating programs with unknown calls. Research report, Teesside University (2010), http:\/\/www.scm.tees.ac.uk\/s.qin\/papers\/unknown.pdf","DOI":"10.1007\/978-3-642-16901-4_13"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-70545-1_41","volume-title":"Computer Aided Verification","author":"S. Magill","year":"2008","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: Thor: A tool for reasoning about shape and arithmetic. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 428\u2013432. Springer, Heidelberg (2008)"},{"key":"13_CR11","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.H. Nguyen","year":"2007","unstructured":"Nguyen, H.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":"13_CR12","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: 31st POPL (January 2004)","DOI":"10.1145\/964001.964024"},{"key":"13_CR13","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th LICS (2002)"},{"key":"13_CR14","volume-title":"COM and DCOM: Microsoft\u2019s vision for distributed objects","author":"R. Sessions","year":"1998","unstructured":"Sessions, R.: COM and DCOM: Microsoft\u2019s vision for distributed objects. John Wiley & Sons, Inc., New York (1998)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Szyperski, C.: Component technology: what, where, and how? In: ICSE (2003)","DOI":"10.1109\/ICSE.2003.1201255"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/11813040_45","volume-title":"FM 2006: Formal Methods","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J.: Verified software grand challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 617\u2013617. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T00:12:29Z","timestamp":1559779949000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}