{"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":1776305058281,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540938996","type":"print"},{"value":"9783540939009","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-93900-9_27","type":"book-chapter","created":{"date-parts":[[2008,12,15]],"date-time":"2008-12-15T04:35:59Z","timestamp":1229315759000},"page":"335-348","source":"Crossref","is-referenced-by-count":63,"title":["Shape-Value Abstraction for Verifying Linearizability"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Vafeiadis","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"27_CR1","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. ACM Trans. on Program. Languages and Systems\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Trans. on Program. Languages and Systems"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"S. Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol.\u00a03235, pp. 97\u2013114. Springer, Heidelberg (2004)"},{"issue":"1","key":"27_CR3","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s00446-004-0115-2","volume":"18","author":"H. Gao","year":"2005","unstructured":"Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free dynamic hash tables with open addressing. Distributed Computing\u00a018(1), 21\u201342 (2005)","journal-title":"Distributed Computing"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11817963_44","volume-title":"Computer Aided Verification","author":"R. Colvin","year":"2006","unstructured":"Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 473\u2013488. Springer, Heidelberg (2006)"},{"key":"27_CR5","first-page":"129","volume-title":"PPoPP 2006","author":"V. Vafeiadis","year":"2006","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP 2006, pp. 129\u2013136. ACM Press, New York (2006)"},{"key":"27_CR6","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)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-69166-2_24","volume-title":"Static Analysis","author":"R. Manevich","year":"2008","unstructured":"Manevich, R., Lev-Ami, T., Ramalingam, G., Sagiv, M., Berdine, J.: Heap decomposition for concurrent shape analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 363\u2013377. Springer, Heidelberg (2008)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-540-70545-1_37","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2008","unstructured":"Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread quantification for concurrent shape analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 399\u2013413. Springer, Heidelberg (2008)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"key":"27_CR10","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321\u2013332 (1983)"},{"key":"27_CR11","first-page":"55","volume-title":"LICS 2002","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"key":"27_CR12","unstructured":"Treiber, R.K.: Systems programming: Coping with parallelism. Technical Report RJ5118, IBM Almaden Res. Ctr. (1986)"},{"key":"#cr-split#-27_CR13.1","unstructured":"Vafeiadis, V.: Fine-grained concurrency verification. Ph.D. dissertation, University of Cambridge (2007);"},{"key":"#cr-split#-27_CR13.2","unstructured":"Also available as Technical Report UCAM-CL-TR-726"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-74061-2_15","volume-title":"Static Analysis","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 233\u2013248. Springer, Heidelberg (2007)"},{"key":"27_CR15","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.W., 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":"27_CR16","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1145\/248052.248106","volume-title":"PODC","author":"M. Michael","year":"1996","unstructured":"Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC, pp. 267\u2013275. ACM Press, New York (1996)"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-36108-1_18","volume-title":"Distributed Computing","author":"T.L. Harris","year":"2002","unstructured":"Harris, T.L., Fraser, K., Pratt, I.A.: A practical multi-word compare-and-swap operation. In: Malkhi, D. (ed.) DISC 2002. LNCS, vol.\u00a02508, pp. 265\u2013279. Springer, Heidelberg (2002)"},{"key":"27_CR18","first-page":"61","volume-title":"PPoPP 2005","author":"L. Wang","year":"2005","unstructured":"Wang, L., Stoller, S.D.: Static analysis of atomicity for programs with non-blocking synchronization. In: PPoPP 2005, pp. 61\u201371. ACM Press, New York (2005)"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Yahav, E., Sagiv, M.: Automatically verifying concurrent queue algorithms. Electronic Notes in Theoretical Computer Science 89(3) (2003)","DOI":"10.1016\/S1571-0661(05)80006-4"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-93900-9_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,4]],"date-time":"2019-03-04T06:49:33Z","timestamp":1551682173000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-93900-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540938996","9783540939009"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-93900-9_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}