{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,14]],"date-time":"2026-09-14T05:18:53Z","timestamp":1789363133789,"version":"build-2803163510"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142949","type":"print"},{"value":"9783642142956","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_40","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"450-464","source":"Crossref","is-referenced-by-count":95,"title":["Automatically Proving Linearizability"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Vafeiadis","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"2","key":"40_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science\u00a082(2), 253\u2013284 (1991)","journal-title":"Theoretical Computer Science"},{"key":"40_CR2","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 linearisability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 477\u2013490. Springer, Heidelberg (2007)"},{"key":"40_CR3","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, S.: Thread quantification for concurrent shape analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 399\u2013413. Springer, Heidelberg (2008)"},{"key":"40_CR4","volume-title":"PLDI 2010","author":"S. Burckhardt","year":"2010","unstructured":"Burckhardt, S., Dern, C., Tan, R., Musuvathi, M.: Line-up: a complete and automatic linearizability checker. In: PLDI 2010. ACM, New York (2010)"},{"key":"40_CR5","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":"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)"},{"key":"40_CR6","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/1065010.1065015","volume-title":"PLDI","author":"T. Elmas","year":"2005","unstructured":"Elmas, T., Tasiran, S., Qadeer, S.: VYRD: verifying concurrent programs by runtime refinement-violation detection. In: PLDI, pp. 27\u201337. ACM, New York (2005)"},{"key":"40_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-00590-9_19","volume-title":"Programming Languages and Systems","author":"I. Filipovi\u0107","year":"2009","unstructured":"Filipovi\u0107, I., O\u2019Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 252\u2013266. Springer, Heidelberg (2009)"},{"issue":"4","key":"40_CR8","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1109\/TSE.2005.47","volume":"31","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Exploiting purity for atomicity. IEEE Trans. Software Eng.\u00a031(4), 275\u2013291 (2005)","journal-title":"IEEE Trans. Software Eng."},{"key":"40_CR9","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. Harris","year":"2002","unstructured":"Harris, T., 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":"40_CR10","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1145\/1007912.1007944","volume-title":"SPAA 2004","author":"D. Hendler","year":"2004","unstructured":"Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. In: SPAA 2004, pp. 206\u2013215. ACM, New York (2004)"},{"issue":"3","key":"40_CR11","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 TOPLAS\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"key":"40_CR12","volume-title":"The art of multiprocessor programming","author":"M.P. Herlihy","year":"2008","unstructured":"Herlihy, M.P., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann, San Francisco (2008)"},{"key":"40_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-05089-3_21","volume-title":"FM 2009: Formal Methods","author":"Y. Liu","year":"2009","unstructured":"Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: Cavalcanti, A., Dams, D. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 321\u2013337. Springer, Heidelberg (2009)"},{"key":"40_CR14","volume-title":"PODC 1996","author":"M. Michael","year":"1996","unstructured":"Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC 1996. ACM, New York (1996)"},{"key":"40_CR15","volume-title":"PODC 2010","author":"P.W. O\u2019Hearn","year":"2010","unstructured":"O\u2019Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: PODC 2010. ACM, New York (2010)"},{"key":"40_CR16","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/292540.292552","volume-title":"POPL 1999","author":"S. Sagiv","year":"1999","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL 1999, pp. 105\u2013118. ACM, New York (1999)"},{"key":"40_CR17","unstructured":"Treiber, R.K.: Systems programming: Coping with parallelism. Tech. report RJ5118, IBM Almaden Res. Ctr. (1986)"},{"key":"40_CR18","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. PhD thesis. Tech. report UCAML-CL-TR-726, Univ. of Cambridge Computer Laboratory (2007)"},{"key":"40_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-540-93900-9_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. Vafeiadis","year":"2009","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 335\u2013348. Springer, Heidelberg (2009)"},{"key":"40_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/978-3-642-11319-2_25","volume-title":"VMCAI 2010","author":"V. Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: RGSep action inference. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 345\u2013361. Springer, Heidelberg (2010)"},{"key":"40_CR21","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Automatically proving linearizability (long version). Tech. report UCAML-CL-TR-778, Univ. of Cambridge Computer Laboratory (2010)","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"40_CR22","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1145\/1375581.1375598","volume-title":"PLDI","author":"M.T. Vechev","year":"2008","unstructured":"Vechev, M.T., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: Gupta, R., Amarasinghe, S.P. (eds.) PLDI, pp. 125\u2013135. ACM, New York (2008)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T00:29:35Z","timestamp":1685665775000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}