{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T21:07:54Z","timestamp":1743109674735,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642376504"},{"type":"electronic","value":"9783642376511"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-642-37651-1_17","type":"book-chapter","created":{"date-parts":[[2013,4,5]],"date-time":"2013-04-05T04:10:01Z","timestamp":1365135001000},"page":"414-445","source":"Crossref","is-referenced-by-count":5,"title":["Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs"],"prefix":"10.1007","author":[{"given":"J.","family":"Kreiker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N.","family":"Rinetzky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reinhard","family":"Wilhelm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E.","family":"Yahav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/11609773_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Arnold","year":"2006","unstructured":"Arnold, G., Manevich, R., Sagiv, M., Shaham, R.: Combining Shape Analyses by Intersecting Abstractions. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 33\u201348. Springer, Heidelberg (2006)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Symp. on Princ. of Prog. Lang. (POPL), pp. 289\u2013300. ACM (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Chase, D.R., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: Conf. on Prog. Lang. Design and Impl., PLDI (1990)","DOI":"10.1145\/93542.93585"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","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, pp. 463\u2013482. Springer, Heidelberg (2003)"},{"key":"17_CR5","first-page":"238","volume-title":"Symp. on Princ. of Prog. Lang. (POPL)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: Symp. on Princ. of Prog. Lang. (POPL), pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E.J. (ed.) Formal Descriptions of Programming Concepts (IFIP WG 2.2, St. Andrews, Canada), pp. 237\u2013277. North-Holland (August 1977)","DOI":"10.1145\/390018.808314"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Deutsch, A.: Interprocedural alias analysis for pointers: Beyond k-limiting. In: Conf. on Prog. Lang. Design and Impl. (PLDI) (1994)","DOI":"10.1145\/178243.178263"},{"key":"17_CR8","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":"17_CR9","doi-asserted-by":"crossref","unstructured":"Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: Symp. on Princ. of Prog. Lang. (POPL) (2005)","DOI":"10.1145\/1040305.1040331"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Symp. on Princ. of Prog. Lang. (POPL) (2001)","DOI":"10.1145\/360204.375719"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-27864-1_19","volume-title":"Static Analysis","author":"B. Jeannet","year":"2004","unstructured":"Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A Relational Approach to Interprocedural Shape Analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 246\u2013264. Springer, Heidelberg (2004)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Int. Conf. on Comp. Construct. (CC) (1992)","DOI":"10.1007\/3-540-55984-1_13"},{"key":"17_CR13","unstructured":"Lev-Ami, T., Sagiv, M.: . TVLA: A framework for Kleene based static analysis. In: International Static Analysis Symposium (SAS) (2000), http:\/\/www.math.tau.ac.il\/~tvla"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Marron, M., Hermenegildo, M., Kapur, D., Stefanovic, D.: Efficient context-sensitive shape analysis with graph based heap models. In: Int. Conf. on Comp. Construct. (CC), pp. 245\u2013259 (2008)","DOI":"10.1007\/978-3-540-78791-4_17"},{"key":"17_CR15","unstructured":"Noble, J., Biddle, R., Tempero, E., Potanin, A., Clarke, D.: Towards a model of encapsulation. In: The First International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO) (2003)"},{"key":"17_CR16","unstructured":"Plotkin, G.D.: A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus (1981)"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Symp. on Princ. of Prog. Lang. (POPL) (1995)","DOI":"10.1145\/199448.199462"},{"key":"17_CR18","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Symp. on Logic in Computer Science (LICS) (2002)"},{"key":"17_CR19","unstructured":"Rinetzky, N.: Interprocedural and Modular Local Heap Shape Analysis. PhD thesis, Tel Aviv University (June 2008)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., Wilhelm, R.: A\u00a0semantics for procedure local heaps and its abstractions. In: Symp. on Princ. of Prog. Lang. (POPL) (2005)","DOI":"10.1145\/1040305.1040330"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-71316-6_16","volume-title":"Programming Languages and Systems","author":"N. Rinetzky","year":"2007","unstructured":"Rinetzky, N., Poetzsch-Heffter, A., Ramalingam, G., Sagiv, M., Yahav, E.: Modular Shape Analysis for Dynamically Encapsulated Programs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 220\u2013236. Springer, Heidelberg (2007)"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Int. Conf. on Comp. Construct. (CC) (2001)","DOI":"10.1007\/3-540-45306-7_10"},{"key":"17_CR23","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":"17_CR24","unstructured":"Rubinstein, S.: On the utility of cutpoints for monitoring program execution. Master\u2019s thesis, Tel Aviv University, Tel Aviv, Israel (2006)"},{"issue":"3","key":"17_CR25","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. Trans. on Prog. Lang. and Syst. (TOPLAS)\u00a024(3), 217\u2013298 (2002)","journal-title":"Trans. on Prog. Lang. and Syst. (TOPLAS)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-44898-5_27","volume-title":"Static Analysis","author":"R. Shaham","year":"2003","unstructured":"Shaham, R., Yahav, E., Kolodner, E.K., Sagiv, M.: Establishing Local Temporal Heap Safety Properties with Applications to Compile-time Memory Management. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 483\u2013503. Springer, Heidelberg (2003)"},{"key":"17_CR27","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, ch.7, pp. 189\u2013234. Prentice-Hall, Englewood Cliffs, NJ (1981)"},{"key":"17_CR28","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","Programming Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37651-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,13]],"date-time":"2022-02-13T03:35:50Z","timestamp":1644723350000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37651-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642376504","9783642376511"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37651-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}