{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T21:38:22Z","timestamp":1790113102809,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642401831","type":"print"},{"value":"9783642401848","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40184-8_18","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T21:50:56Z","timestamp":1374529856000},"page":"242-256","source":"Crossref","is-referenced-by-count":41,"title":["Aspect-Oriented Linearizability Proofs"],"prefix":"10.1007","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ali","family":"Sezgin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 324\u2013338. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"18_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 linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 477\u2013490. Springer, Heidelberg (2007)"},{"issue":"2","key":"18_CR3","first-page":"93","volume":"137","author":"R. Colvin","year":"2005","unstructured":"Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. ENTCS\u00a0137(2), 93\u2013110 (2005)","journal-title":"ENTCS"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-642-21437-0_25","volume-title":"FM 2011: Formal Methods","author":"J. Derrick","year":"2011","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Verifying linearisability with potential linearisation points. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 323\u2013337. Springer, Heidelberg (2011)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-04355-0_28","volume-title":"Distributed Computing","author":"S. Doherty","year":"2009","unstructured":"Doherty, S., Moir, M.: Nonblocking algorithms and backward simulation. In: Keidar, I. (ed.) DISC\u201909. LNCS, vol. 5805, pp. 274\u2013288. Springer (2009)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Hendler, D., Incze, I., Shavit, N., Tzafrir, M.: Flat combining and the synchronization-parallelism tradeoff. In: SPAA 2010, pp. 355\u2013364. ACM (2010)","DOI":"10.1145\/1810479.1810540"},{"key":"18_CR7","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc. (2008)"},{"issue":"3","key":"18_CR8","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. Program. Lang. Syst.\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-77096-1_29","volume-title":"Principles of Distributed Systems","author":"M. Hoffman","year":"2007","unstructured":"Hoffman, M., Shalev, O., Shavit, N.: The baskets queue. In: Tovar, E., Tsigas, P., Fouchal, H. (eds.) OPODIS 2007. LNCS, vol.\u00a04878, pp. 401\u2013414. Springer, Heidelberg (2007)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-540-30186-8_9","volume-title":"Distributed Computing","author":"E. Ladan-Mozes","year":"2004","unstructured":"Ladan-Mozes, E., Shavit, N.: An optimistic approach to lock-free FIFO queues. In: Guerraoui, R. (ed.) DISC 2004. LNCS, vol.\u00a03274, pp. 117\u2013131. Springer, Heidelberg (2004)"},{"key":"18_CR11","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.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 321\u2013337. Springer, Heidelberg (2009)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Moir, M., Nussbaum, D., Shalev, O., Shavit, N.: Using elimination to implement scalable and lock-free FIFO queues. In: SPAA 2005, pp. 253\u2013262. ACM (2005)","DOI":"10.1145\/1073970.1074013"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-31424-7_21","volume-title":"Computer Aided Verification","author":"G. Schellhorn","year":"2012","unstructured":"Schellhorn, G., Wehrheim, H., Derrick, J.: How to prove algorithms linearisable. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 243\u2013259. Springer, Heidelberg (2012)"},{"key":"18_CR14","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":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V. Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 450\u2013464. Springer, Heidelberg (2010)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-11319-2_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","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)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2013 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40184-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T22:51:58Z","timestamp":1557960718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40184-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401831","9783642401848"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40184-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}