{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:25Z","timestamp":1725511885811},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540713142"},{"type":"electronic","value":"9783540713166"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-71316-6_16","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:58:28Z","timestamp":1184590708000},"page":"220-236","source":"Crossref","is-referenced-by-count":8,"title":["Modular Shape Analysis for Dynamically Encapsulated Programs"],"prefix":"10.1007","author":[{"given":"N.","family":"Rinetzky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Poetzsch-Heffter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E.","family":"Yahav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45937-5_13","volume-title":"Compiler Construction","author":"P. Cousot","year":"2002","unstructured":"Cousot, P., Cousot, R.: Modular Static Program Analysis. In: Horspool, R.N. (ed.) CC 2002 and ETAPS 2002. LNCS, vol.\u00a02304, Springer, Heidelberg (2002)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","first-page":"547","volume-title":"Computer Aided Verification","author":"M. Sagiv","year":"2006","unstructured":"Sagiv, M., Immerman, N., Lev-Ami, T.: Abstraction for Shape Analysis with Fast and Precise Transformers. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 547\u2013561. Springer, Heidelberg (2006)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","first-page":"181","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Ramalingam","year":"2005","unstructured":"Ramalingam, G., et al.: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Yang","year":"2006","unstructured":"Yang, H., O\u2019Hearn, P.W., Distefano, D.: A Local Shape Analysis Based on Separation Logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/b107380","volume-title":"Static Analysis","author":"M. Sagiv","year":"2005","unstructured":"Sagiv, M., Rinetzky, N., 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":"16_CR6","series-title":"Lecture Notes in Computer Science","first-page":"240","volume-title":"Static Analysis","author":"B. Cook","year":"2006","unstructured":"Cook, B., Berdine, J., Gotsman, A.: Interprocedural Shape Analysis with Separated Heap Abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 240\u2013260. Springer, Heidelberg (2006)"},{"key":"16_CR7","unstructured":"Rinetzky, N., et al.: Componentized heap abstractions. Tech. Rep. 164, Tel Aviv University (2006)"},{"issue":"1","key":"16_CR8","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"R.E. Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng.\u00a012(1), 157\u2013171 (1986)","journal-title":"IEEE Trans. Software Eng."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., et al.: Modular shape analysis for dynamically encapsulated programs. Tech. Rep. 107, Tel Aviv University (2006)","DOI":"10.1007\/978-3-540-71316-6_16"},{"key":"16_CR10","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS (2002)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., et al.: A\u00a0semantics for procedure local heaps and its abstractions. In: POPL (2005)","DOI":"10.1145\/1040305.1040330"},{"key":"16_CR12","unstructured":"Plotkin, G.D.: A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus (1981)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Compiler Construction","author":"J. Knoop","year":"1992","unstructured":"Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol.\u00a0641, Springer, Heidelberg (1992)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_3","volume-title":"Static Analysis","author":"F. Logozzo","year":"2003","unstructured":"Logozzo, F.: Class-level modular analysis for object oriented languages. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/978-3-540-24622-0_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F. Logozzo","year":"2004","unstructured":"Logozzo, F.: Automatic Inference of Class Invariants. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 211\u2013222. Springer, Heidelberg (2004)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Aggarwal, A., Randall, K.: Related field analysis. In: PLDI (2001)","DOI":"10.1145\/378795.378850"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-540-31985-6_16","volume-title":"Compiler Construction","author":"P. Lam","year":"2005","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Hob: A Tool for Verifying Data\u00a0Structure\u00a0Consistency. In: Bodik, R. (ed.) CC 2005. LNCS, vol.\u00a03443, pp. 237\u2013241. Springer, Heidelberg (2005)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","first-page":"157","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., et al.: Field Constraint Analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 157\u2013173. Springer, Heidelberg (2005)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","first-page":"246","volume-title":"Static Analysis","author":"M. Sagiv","year":"2004","unstructured":"Sagiv, M., et al.: A Relational Approach to Interprocedural Shape Analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 246\u2013264. Springer, Heidelberg (2004)"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_26","volume-title":"Static Analysis","author":"S. Chong","year":"2003","unstructured":"Chong, S., Rugina, R.: Static analysis of accessed regions in recursive data structures. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL (2005)","DOI":"10.1145\/1040305.1040331"},{"key":"16_CR23","unstructured":"Noble, J., et al.: Towards a model of encapsulation. In: IWACO (2003)"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Zhao, T., Noble, J., Vitek, J.: Scoped types for real-time java. In: RTSS (2004)","DOI":"10.1109\/REAL.2004.51"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"D. Clarke","year":"2003","unstructured":"Clarke, D., Wrigstad, T.: External uniqueness is unique enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, Springer, Heidelberg (2003)"},{"issue":"6","key":"16_CR26","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1002\/spe.370","volume":"31","author":"J. Boyland","year":"2001","unstructured":"Boyland, J.: Alias burying: unique variables without destructive reads. Softw. Pract. Exper.\u00a031(6), 533\u2013553 (2001)","journal-title":"Softw. Pract. Exper."},{"issue":"6","key":"16_CR27","doi-asserted-by":"crossref","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., et al.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6), 27\u201356 (2004)","journal-title":"Journal of Object Technology"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11693024_9","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2006","unstructured":"Leino, K.R.M., M\u00fcller, P.: A Verification Methodology for Model Fields. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, pp. 115\u2013130. Springer, Heidelberg (2006)"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: POPL (2004)","DOI":"10.1145\/964001.964024"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Bierman, G., Parkinson, M.: Separation logic and abstractions. In: POPL (2005)","DOI":"10.1145\/1040305.1040326"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71316-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:49:58Z","timestamp":1556668198000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71316-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540713142","9783540713166"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71316-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}