{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:18Z","timestamp":1776305058072,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540691631","type":"print"},{"value":"9783540691662","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69166-2_24","type":"book-chapter","created":{"date-parts":[[2008,7,13]],"date-time":"2008-07-13T09:25:03Z","timestamp":1215941103000},"page":"363-377","source":"Crossref","is-referenced-by-count":22,"title":["Heap Decomposition for Concurrent Shape Analysis"],"prefix":"10.1007","author":[{"given":"Roman","family":"Manevich","sequence":"first","affiliation":[]},{"given":"Tal","family":"Lev-Ami","sequence":"additional","affiliation":[]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[]},{"given":"Ganesan","family":"Ramalingam","sequence":"additional","affiliation":[]},{"given":"Josh","family":"Berdine","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-73368-3_49","volume-title":"Computer Aided Verification","author":"D. Amit","year":"2007","unstructured":"Amit, D., Rinetzky, N., Reps, T., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 477\u2013490. Springer, Heidelberg (2007)"},{"issue":"2","key":"24_CR2","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.entcs.2005.04.026","volume":"137","author":"R. Colvin","year":"2005","unstructured":"Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. Electr. Notes Theor. Comput. Sci.\u00a0137(2), 93\u2013110 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Doherty, S., Detlefs, D.L., Groves, L., Flood, C.H., Luchangco, V., Martin, P.A., Moir, M., Shavit, N., Steele Jr., G.L.: DCAS is not a silver bullet for nonblocking algorithm design. In: SPAA, pp. 216\u2013224 (2004)","DOI":"10.1145\/1007912.1007945"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Applying Formal Methods: Testing, Performance, and M\/E-Commerce","author":"S. Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: N\u00fa\u00f1ez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol.\u00a03236, pp. 97\u2013114. Springer, Heidelberg (2004)"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI, pp. 266\u2013277 (2007)","DOI":"10.1145\/1250734.1250765"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL, pp. 310\u2013323 (2005)","DOI":"10.1145\/1040305.1040331"},{"issue":"3","key":"24_CR7","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M.P. Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. TOPLAS\u00a012(3), 463\u2013492 (1990)","journal-title":"TOPLAS"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A framework for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013301. Springer, Heidelberg (2000)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Manevich, R., Berdine, J., Cook, B., Ramalingam, G., Sagiv, M.: Shape analysis by graph decomposition. In: TACAS, pp. 3\u201318 (2007)","DOI":"10.1007\/978-3-540-71209-1_3"},{"key":"24_CR10","unstructured":"Manevich, R., Lev-Ami, T., Sagiv, M., Ramalingam, G., Berdine, J.: Heap decomposition for concurrent shape analysis. Technical Report TR-2008-01-85453, Tel Aviv University (January 2008), http:\/\/www.cs.tau.ac.il\/rumster\/TR-2007-11-85453.pdf"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-3-540-27864-1_20","volume-title":"Static Analysis","author":"R. Manevich","year":"2004","unstructured":"Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 265\u2013279. Springer, Heidelberg (2004)"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC, pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"24_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"issue":"3","key":"24_CR14","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. ACM Transactions on Programming Languages and Systems\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR15","unstructured":"Treiber, R.K.: Systems programming: Coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center (April 1986)"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. draft (2008)","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPOPP, pp. 129\u2013136 (2006)","DOI":"10.1145\/1122971.1122992"},{"issue":"3","key":"24_CR18","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/373243.360206","volume":"36","author":"E. Yahav","year":"2001","unstructured":"Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. ACM SIGPLAN Notices\u00a036(3), 27\u201340 (2001)","journal-title":"ACM SIGPLAN Notices"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: PLDI, pp. 25\u201334 (2004)","DOI":"10.1145\/996841.996846"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69166-2_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:30:14Z","timestamp":1620016214000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69166-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540691631","9783540691662"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69166-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}