{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:20Z","timestamp":1776305060939,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662534120","type":"print"},{"value":"9783662534137","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-53413-7_4","type":"book-chapter","created":{"date-parts":[[2016,8,30]],"date-time":"2016-08-30T07:57:11Z","timestamp":1472543831000},"page":"61-83","source":"Crossref","is-referenced-by-count":4,"title":["Automated Verification of Linearization Policies"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong Quy","family":"Trinh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,31]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/978-3-642-36742-7_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2013","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 (ETAPS 2013). LNCS, vol. 7795, pp. 324\u2013338. Springer, Heidelberg (2013)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 4590, pp. 477\u2013490. Springer, Heidelberg (2007)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 5123, pp. 399\u2013413. Springer, Heidelberg (2008)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","first-page":"95","volume-title":"Automata, Languages and Programming","author":"S Guha","year":"2002","unstructured":"Guha, S., Indyk, P., Muthukrishnan, S.M., Strauss, M.J.: On reducing linearizability to state reachability. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 95\u2013107. Springer, Heidelberg (2002)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/978-3-642-37036-6_17","volume-title":"Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 290\u2013309. Springer, Heidelberg (2013)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"475","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 algorithm. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 475\u2013488. Springer, Heidelberg (2006)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-319-06410-9_15","volume-title":"FM 2014: Formal Methods","author":"J Derrick","year":"2014","unstructured":"Derrick, J., Dongol, B., Schellhorn, G., Tofan, B., Travkin, O., Wehrheim, H.: Quiescent consistency: defining and verifying relaxed linearizability. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 200\u2013214. Springer, Heidelberg (2014)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Doherty, S., Detlefs, D., Groves, L., Flood, C., Luchangco, V., Martin, P., Moir, M., Shavit, N., Steele Jr., G.: DCAS is not a silver bullet for nonblocking algorithm design. In: SPAA 2004, pp. 216\u2013224. ACM (2004)","DOI":"10.1145\/1007912.1007945"},{"key":"4_CR9","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\u00a0practical lock-free queue algorithm. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97\u2013114. Springer, Heidelberg (2004)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/3-540-45414-4_21","volume-title":"Distributed Computing","author":"TL Harris","year":"2001","unstructured":"Harris, T.L.: A pragmatic implementation of non-blocking linked-lists. In: Welch, J.L. (ed.) DISC 2001. LNCS, vol. 2180, pp. 300\u2013314. Springer, Heidelberg (2001)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-36108-1_18","volume-title":"Distributed Computing","author":"TL 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. 2508, pp. 265\u2013279. Springer, Heidelberg (2002)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/11795490_3","volume-title":"Principles of Distributed Systems","author":"S Heller","year":"2006","unstructured":"Heller, S., Herlihy, M.P., Luchangco, V., Moir, M., Scherer III, W.N., Shavit, N.N.: A lazy concurrent list-based set algorithm. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol. 3974, pp. 3\u201316. Springer, Heidelberg (2006)"},{"issue":"1","key":"4_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jpdc.2009.08.011","volume":"70","author":"D Hendler","year":"2010","unstructured":"Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. J. Parallel Distrib. Comput. 70(1), 1\u201312 (2010)","journal-title":"J. Parallel Distrib. Comput."},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/978-3-642-40184-8_18","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"TA Henzinger","year":"2013","unstructured":"Henzinger, T.A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. LNCS, vol. 8052, pp. 242\u2013256. Springer, Heidelberg (2013)"},{"key":"4_CR16","volume-title":"The Art of Multiprocessor Programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, San Francisco (2008)"},{"issue":"3","key":"4_CR17","doi-asserted-by":"crossref","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. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: PLDI, pp. 459\u2013470. ACM (2013)","DOI":"10.1145\/2491956.2462189"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/978-3-540-30579-8_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Manevich","year":"2005","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"key":"4_CR20","unstructured":"Michael, M., Scott, M.: Correction of a memory management method for lock-free data structures. Technical Report TR599, University of Rochester, Rochester, NY, USA (1995)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC, pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Michael, M.M.: High performance dynamic lock-free hash tables and list-based sets. In: SPAA, pp. 73\u201382 (2002)","DOI":"10.1145\/564870.564881"},{"key":"4_CR23","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 (2005)","DOI":"10.1145\/1073970.1074013"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: PODC, pp. 85\u201394 (2010)","DOI":"10.1145\/1835698.1835722"},{"issue":"4","key":"4_CR25","doi-asserted-by":"crossref","first-page":"31:1","DOI":"10.1145\/2629496","volume":"15","author":"G Schellhorn","year":"2014","unstructured":"Schellhorn, G., Derrick, J., Wehrheim, H.: A sound, complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Log. 15(4), 31:1\u201331:37 (2014)","journal-title":"ACM Trans. Comput. Log."},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 7358, pp. 243\u2013259. Springer, Heidelberg (2012)"},{"key":"4_CR27","unstructured":"Treiber, R.: Systems programming: Coping with parallelism. Technical Report RJ5118, IBM Almaden Res. Ctr. (1986)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: POPL 2013, pp. 343\u2013356 (2013)","DOI":"10.1145\/2429069.2429111"},{"key":"4_CR29","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. PhD thesis, University of Cambridge (2008)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 5403, pp. 335\u2013348. Springer, Heidelberg (2009)"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6174, pp. 450\u2013464. Springer, Heidelberg (2010)"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/978-3-642-14295-6_41","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2010","unstructured":"\u010cern\u00fd, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 465\u2013479. Springer, Heidelberg (2010)"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/978-3-642-02652-2_21","volume-title":"Model Checking Software","author":"M Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: P\u0103s\u0103reanu, C.S. (ed.) Model Checking Software. LNCS, vol. 5578, pp. 261\u2013278. Springer, Heidelberg (2009)"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: PLDI, pp. 125\u2013135 (2008)","DOI":"10.1145\/1375581.1375598"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-642-41527-2_17","volume-title":"Distributed Computing","author":"K Zhang","year":"2013","unstructured":"Zhang, K., Zhao, Y., Yang, Y., Liu, Y., Spear, M.: Practical non-blocking unordered lists. In: Afek, Y. (ed.) DISC 2013. LNCS, vol. 8205, pp. 239\u2013253. Springer, Heidelberg (2013)"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","first-page":"3","volume-title":"Computer Aided Verification","author":"H Zhu","year":"2015","unstructured":"Zhu, H., Petri, G., Jagannathan, S.: Poling: SMT aided linearizability proofs. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 3\u201319. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-53413-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T17:38:33Z","timestamp":1498325913000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-53413-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662534120","9783662534137"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-53413-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}