{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:17Z","timestamp":1776305057388,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540733676","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_49","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"477-490","source":"Crossref","is-referenced-by-count":58,"title":["Comparison Under Abstraction for Verifying Linearizability"],"prefix":"10.1007","author":[{"given":"Daphna","family":"Amit","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eran","family":"Yahav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"49_CR1","doi-asserted-by":"crossref","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. Trans. on Prog. Lang. and Syst.\u00a012(3) (1990)","DOI":"10.1145\/78969.78972"},{"key":"49_CR2","doi-asserted-by":"crossref","unstructured":"Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC (1996)","DOI":"10.1145\/248052.248106"},{"key":"49_CR3","unstructured":"Treiber, R.K.: Systems programming: Coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center (1986)"},{"key":"49_CR4","unstructured":"Amit, D.: Comparison under abstraction for verifying linearizability. Master\u2019s thesis, Tel Aviv University (2007), available at http:\/\/www.cs.tau.ac.il\/~amitdaph"},{"key":"49_CR5","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst. (2002)","DOI":"10.1145\/514188.514190"},{"key":"49_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_35","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"49_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Gopan","year":"2004","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T.W., Sagiv, S.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, Springer, Heidelberg (2004)"},{"key":"49_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T.W., Sagiv, M.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, Springer, Heidelberg (2005)"},{"key":"49_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"T. Reps","year":"2003","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite Differencing of Logical Formulas for Static Analysis. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, Springer, Heidelberg (2003)"},{"key":"49_CR10","doi-asserted-by":"crossref","unstructured":"Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. In: POPL (2001)","DOI":"10.1145\/360204.360206"},{"key":"49_CR11","doi-asserted-by":"crossref","unstructured":"Michael, M.M.: Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst.\u00a015(6) (2004)","DOI":"10.1109\/TPDS.2004.8"},{"key":"49_CR12","volume-title":"Electronic Notes in Theoretical Computer Science","author":"E. Yahav","year":"2003","unstructured":"Yahav, E., Sagiv, M.: Automatically verifying concurrent queue algorithms. In: Electronic Notes in Theoretical Computer Science, vol.\u00a089, Elsevier, Amsterdam (2003)"},{"key":"49_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A framework for Kleene based static analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, Springer, Heidelberg (2000)"},{"key":"49_CR14","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, J., Peled, O.: Model checking. MIT Press, Cambridge, MA, USA (1999)"},{"key":"49_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Applying Formal Methods: Testing, Performance, and M\/E-Commerce","author":"S. Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: N\u00fa\u00f1ez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol.\u00a03236, Springer, Heidelberg (2004)"},{"key":"49_CR16","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP (2006)","DOI":"10.1145\/1122971.1122992"},{"key":"49_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C.: Verifying commit-atomicity using model-checking. In: Graf, S., Mounier, L. (eds.) Model Checking Software. LNCS, vol.\u00a02989, Springer, Heidelberg (2004)"},{"key":"49_CR18","doi-asserted-by":"crossref","unstructured":"Wang, L., Stoller, S.D.: Static analysis of atomicity for programs with non-blocking synchronization. In: PPOPP (2005)","DOI":"10.1145\/1065944.1065953"},{"key":"49_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a04144, Springer, Heidelberg (2006)"},{"key":"49_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"H. Gao","year":"2004","unstructured":"Gao, H., Hesselink, W.H.: A formal reduction for lock-free parallel algorithms. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_49.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:38Z","timestamp":1619518118000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_49","relation":{},"subject":[]}}