{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:48:05Z","timestamp":1770274085765,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642367410","type":"print"},{"value":"9783642367427","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36742-7_23","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:41:56Z","timestamp":1361216516000},"page":"324-338","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["An Integrated Specification and Verification Technique for Highly Concurrent Data Structures"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Haziza","sequence":"additional","affiliation":[]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[]},{"given":"Ahmed","family":"Rezine","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"23_CR1","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10009-011-0212-z","volume":"14","author":"P. Abdulla","year":"2012","unstructured":"Abdulla, P., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for LTL(MSO). STTT\u00a014(2), 223\u2013241 (2012)","journal-title":"STTT"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-35873-9_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P.A. Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the Price of Few (Parameterized Verification through View Abstraction). In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 476\u2013495. Springer, Heidelberg (2013)"},{"key":"23_CR3","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)"},{"key":"23_CR4","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, M.: Thread Quantification for Concurrent Shape Analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 399\u2013413. Springer, Heidelberg (2008)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11609773_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Bingham","year":"2006","unstructured":"Bingham, J., Rakamari\u0107, Z.: A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 207\u2013221. Springer, Heidelberg (2006)"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Proc. of PLDI 2010, pp. 330\u2013340. ACM (2010)","DOI":"10.1145\/1809028.1806634"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a06174, pp. 465\u2013479. Springer, Heidelberg (2010)"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a04144, pp. 475\u2013488. Springer, Heidelberg (2006)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"23_CR10","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: Proc. of SPAA 2004, pp. 216\u2013224. ACM (2004)","DOI":"10.1145\/1007912.1007945"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a03235, pp. 97\u2013114. Springer, Heidelberg (2004)"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-642-12002-2_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Elmas","year":"2010","unstructured":"Elmas, T., Qadeer, S., Sezgin, A., Subasi, O., Tasiran, S.: Simplifying Linearizability Proofs with Reduction and Abstraction. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 296\u2013311. Springer, Heidelberg (2010)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-00768-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Emmi","year":"2009","unstructured":"Emmi, M., Jhala, R., Kohler, E., Majumdar, R.: Verifying Reference Counting Implementations. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 352\u2013367. Springer, Heidelberg (2009)"},{"issue":"2","key":"23_CR14","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.scico.2007.12.001","volume":"71","author":"C. Flanagan","year":"2008","unstructured":"Flanagan, C., Freund, S.: Atomizer: A dynamic atomicity checker for multithreaded programs. Science of Computer Programming\u00a071(2), 89\u2013109 (2008)","journal-title":"Science of Computer Programming"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forest automata for verification of heap manipulation. Formal Methods in System Design, 1\u201324 (2012)","DOI":"10.1007\/s10703-012-0150-8"},{"issue":"3","key":"23_CR16","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. ACM Trans. Program. Lang. Syst.\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR17","unstructured":"IBM. System\/370 principles of operation (1983)"},{"issue":"6","key":"23_CR18","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s10009-011-0197-7","volume":"13","author":"N. Kidd","year":"2011","unstructured":"Kidd, N., Reps, T., Dolby, J., Vaziri, M.: Finding concurrency-related bugs using random isolation. STTT\u00a013(6), 495\u2013518 (2011)","journal-title":"STTT"},{"key":"23_CR19","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":"23_CR20","doi-asserted-by":"crossref","unstructured":"Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proc. 15th ACM Symp. on PoDC, pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Michael, M.M.: Safe memory reclamation for dynamic lock-free objects using atomic reads and writes. In: Proc. 21st Annual Symp. on PoDC, pp. 21\u201330 (2002)","DOI":"10.1145\/571825.571829"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Naik, M., Aiken, A., Whaley, J.: Effective static race detection for java. In: Proc. of PLDI 2006, pp. 308\u2013319. ACM (2006)","DOI":"10.1145\/1133981.1134018"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Naik, M., Park, C.-S., Sen, K., Gay, D.: Effective static deadlock detection. In: Proc. of ICSE, pp. 386\u2013396. IEEE (2009)","DOI":"10.1109\/ICSE.2009.5070538"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-10672-9_5","volume-title":"Programming Languages and Systems","author":"M. Segalov","year":"2009","unstructured":"Segalov, M., Lev-Ami, T., Manevich, R., Ganesan, R., Sagiv, M.: Abstract Transformers for Thread Correlation Analysis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 30\u201346. Springer, Heidelberg (2009)"},{"key":"23_CR25","unstructured":"Shacham, O.: Verifying Atomicity of Composed Concurrent Operations. PhD thesis, Department of Computer Science, Tel Aviv University (2012)"},{"key":"23_CR26","unstructured":"Treiber, R.: Systems programming: Coping with parallelism. Technical Report RJ5118, IBM Almaden Res. Ctr. (1986)"},{"key":"23_CR27","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":"23_CR28","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":"23_CR29","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)"},{"key":"23_CR30","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. of LICS 1986, pp. 332\u2013344 (June 1986)"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: Proc. of PLDI 2008, pp. 125\u2013135. ACM (2008)","DOI":"10.1145\/1379022.1375598"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) SPIN 2009. LNCS, vol.\u00a05578, pp. 261\u2013278. Springer, Heidelberg (2009)"},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Wang, L., Stoller, S.: Static analysis of atomicity for programs with non-blocking synchronization. In: Proc. of PPOPP 2005, pp. 61\u201371. ACM (2005)","DOI":"10.1145\/1065944.1065953"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic (extended abstract). In: Proc. of POPL 1986, pp. 184\u2013193 (1986)","DOI":"10.1145\/512644.512661"},{"key":"23_CR35","doi-asserted-by":"crossref","unstructured":"Yahav, E., Sagiv, S.: Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci.\u00a089(3) (2003)","DOI":"10.1016\/S1571-0661(05)80006-4"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36742-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,1]],"date-time":"2020-06-01T00:02:54Z","timestamp":1590969774000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36742-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642367410","9783642367427"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36742-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}