{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T22:50:51Z","timestamp":1789944651303,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662486528","type":"print"},{"value":"9783662486535","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48653-5_25","type":"book-chapter","created":{"date-parts":[[2015,10,2]],"date-time":"2015-10-02T18:46:01Z","timestamp":1443811561000},"page":"371-387","source":"Crossref","is-referenced-by-count":20,"title":["Modular Verification of Concurrency-Aware Linearizability"],"prefix":"10.1007","author":[{"given":"Nir","family":"Hemed","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,11,5]]},"reference":[{"issue":"4","key":"25_CR1","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s00446-013-0185-0","volume":"26","author":"Y Afek","year":"2013","unstructured":"Afek, Y., Hakimi, M., Morrison, A.: Fast and scalable rendezvousing. Distributed Computing 26(4), 243\u2013269 (2013)","journal-title":"Distributed Computing"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Borowsky, E., Gafni, E.: Immediate atomic snapshots and fast renaming. In: Anderson, J., Toueg, S. (eds.) PODC (1993)","DOI":"10.1145\/164051.164056"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Castaneda, A., Rajsbaum, S., Raynal, M.: Specifying concurrent problems: beyond linearizability and up to tasks. In: DISC (2015)","DOI":"10.1007\/978-3-662-48653-5_28"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P Rocha Pinto da","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504\u2013528. Springer, Heidelberg (2010)"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-39799-8_11","volume-title":"Computer Aided Verification","author":"C Dr\u0103goi","year":"2013","unstructured":"Dr\u0103goi, C., Gupta, A., Henzinger, T.A.: Automatic linearizability proofs of concurrent objects with cooperating updates. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 174\u2013190. Springer, Heidelberg (2013)"},{"issue":"51-52","key":"25_CR7","doi-asserted-by":"crossref","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"Ivana Filipovi\u0107","year":"2010","unstructured":"Filipovic, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51\u201352) (2010)","journal-title":"Theoretical Computer Science"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Hemed, N., Rinetzky, N.: Brief announcement: concurrency-aware linearizability. In: Halld\u00f3rsson, M.M., Dolev, S. (eds.) PODC, pp. 209\u2013211. ACM (2014)","DOI":"10.1145\/2611462.2611513"},{"key":"25_CR9","unstructured":"Hemed, N., Rinetzky, N., Vafeiadis, V.: Modular verification of concurrency-aware linearizability (2015). http:\/\/www.cs.tau.ac.il\/nirh\/disc15-ext.pdf"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. In: SPAA (2004)","DOI":"10.1145\/1007912.1007944"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-642-15763-9_8","volume-title":"Distributed Computing","author":"D Hendler","year":"2010","unstructured":"Hendler, D., Incze, I., Shavit, N., Tzafrir, M.: Scalable flat-combining based synchronous queues. In: Lynch, N.A., Shvartsman, A.A. (eds.) DISC 2010. LNCS, vol. 6343, pp. 79\u201393. Springer, Heidelberg (2010)"},{"issue":"3","key":"25_CR12","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"Trans. Program. Lang. Syst."},{"issue":"10","key":"25_CR13","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-30186-8_13","volume-title":"Distributed Computing","author":"WN Scherer III","year":"2004","unstructured":"Scherer III, W.N., Scott, M.L.: Nonblocking concurrent data structures with condition synchronization. In: Guerraoui, R. (ed.) DISC 2004. LNCS, vol. 3274, pp. 174\u2013187. Springer, Heidelberg (2004)"},{"key":"25_CR15","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress (1983)"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL (2015)","DOI":"10.1145\/2676726.2676980"},{"key":"25_CR17","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, pp. 253\u2013262. ACM (2005)","DOI":"10.1145\/1073970.1074013"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Neiger, G.: Set-linearizability. In: Anderson, J.H., Peleg, D., Borowsky, E. (eds.) PODC 1994, pp. 396\u2013396. ACM (1994)","DOI":"10.1145\/197917.198176"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"PW O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, p. 1. Springer, Heidelberg (2001)"},{"issue":"4","key":"25_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2629496","volume":"15","author":"Gerhard Schellhorn","year":"2014","unstructured":"Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Logic 15(4) (2014)","journal-title":"ACM Transactions on Computational Logic"},{"key":"25_CR21","unstructured":"Scherer III, W.N., Lea, D., Scott, M.L.: A scalable elimination-based exchange channel. SCOOL (2005)"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Scherer III, W.N., Lea, D., Scott, M.L.: Scalable synchronous queues. In: Torrellas, J., Chatterjee, S. (eds.) PPoPP 2006, pp. 147\u2013156. ACM (2006)","DOI":"10.1145\/1122971.1122994"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-662-46669-8_14","volume-title":"Programming Languages and Systems","author":"I Sergey","year":"2015","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Specifying and verifying concurrent algorithms with histories and subjectivity. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 333\u2013358. Springer, Heidelberg (2015)"},{"issue":"6","key":"25_CR24","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/s002240000072","volume":"30","author":"N Shavit","year":"1997","unstructured":"Shavit, N., Touitou, D.: Elimination trees and the construction of pools and stacks. Theory Comput. Syst. 30(6), 645\u2013670 (1997)","journal-title":"Theory Comput. Syst."},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 149\u2013168. Springer, Heidelberg (2014)"},{"key":"25_CR26","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge (2008)"}],"container-title":["Lecture Notes in Computer Science","Distributed Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48653-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,31]],"date-time":"2019-08-31T02:13:39Z","timestamp":1567217619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48653-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662486528","9783662486535"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48653-5_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}