{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T00:17:48Z","timestamp":1767140268353,"version":"build-2238731810"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2016,3,16]],"date-time":"2016-03-16T00:00:00Z","timestamp":1458086400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,3,16]],"date-time":"2016-03-16T00:00:00Z","timestamp":1458086400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s10009-016-0415-4","type":"journal-article","created":{"date-parts":[[2016,3,18]],"date-time":"2016-03-18T12:05:18Z","timestamp":1458302718000},"page":"549-563","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["An integrated specification and\n              verification technique for highly concurrent data structures"],"prefix":"10.1007","volume":"19","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Haziza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmed","family":"Rezine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,3,16]]},"reference":[{"issue":"2","key":"415_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.:\n                  Regular model checking for LTL(MSO). STTT 14(2),\n                  223\u2013241 (2012)","journal-title":"STTT"},{"key":"415_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few. In:\n                  VMCAI, pp. 476\u2013495. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-35873-9_28"},{"key":"415_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An\n                  integrated specification and verification technique for highly concurrent data\n                  structures. In: TACAS, vol. 7795, LNCS, pp. 324\u2013338. Springer, Berlin\n                  (2013)","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"415_CR4","doi-asserted-by":"crossref","unstructured":"Amit, D., Rinetzky, N., Reps, T., Sagiv, M., Yahav, E.: Comparison\n                  under abstraction for verifying linearizability. In: Proc. of CAV\u201907. LNCS, vol.\n                  4590, pp. 477\u2013490. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"415_CR5","doi-asserted-by":"crossref","unstructured":"Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, S.:\n                  Thread quantification for concurrent shape analysis. In: Proceedings of CAV\u201908.\n                  LNCS, vol. 5123, pp. 399\u2013413. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1_37"},{"key":"415_CR6","doi-asserted-by":"crossref","unstructured":"Bingham, J., Rakamaric, Z.: A logic and decision procedure for\n                  predicate abstraction of heap-manipulating programs. In: Proc. of VMCAI\u201906. LNCS,\n                  vol. 3855, pp. 207\u2013221. Springer, Berlin (2006)","DOI":"10.1007\/11609773_14"},{"key":"415_CR7","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a\n                  complete and automatic linearizability checker. In: Proceedings of PLDI\u201910, pp.\n                  330\u2013340. ACM, New York (2010)","DOI":"10.1145\/1809028.1806634"},{"key":"415_CR8","doi-asserted-by":"crossref","unstructured":"Cern\u00fd, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.:\n                  Model checking of linearizability of concurrent list implementations. In: Proc. of\n                  CAV\u201910, LNCS, vol. 6174, pp. 465\u2013479. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_41"},{"key":"415_CR9","doi-asserted-by":"crossref","unstructured":"Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal\n                  verification of a lazy concurrent list-based set algorithm. In: Proceedings of\n                  CAV\u201906. LNCS, vol. 4144, pp. 475\u2013488. Springer, Berlin (2006)","DOI":"10.1007\/11817963_44"},{"key":"415_CR10","doi-asserted-by":"crossref","unstructured":"Dill, D.: Timing assumptions and verification of finite-state\n                  concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for\n                  Finite-State Systems, vol. 407. LNCS. Springer, Berlin (1989)","DOI":"10.1007\/3-540-52148-8_17"},{"key":"415_CR11","doi-asserted-by":"crossref","unstructured":"Doherty, S., Detlefs, D., Groves, L., Flood, C., Luchangco, V.,\n                  Martin, P., Moir, M., Shavit, N., Jr. G.S.: Dcas is not a silver bullet for\n                  nonblocking algorithm design. In: Proceedings of SPAA\u201904, pp. 216\u2013224. ACM, New\n                  York (2004)","DOI":"10.1145\/1007912.1007945"},{"key":"415_CR12","doi-asserted-by":"crossref","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal\n                  verification of a practical lock-free queue algorithm. In: Proceedings of\n                  FORTE\u201904. LNCS, vol. 3235, pp. 97\u2013114. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"415_CR13","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Sezgin, A., Subasi, O., Tasiran, S.:\n                  Simplifying linearizability proofs with reduction and abstraction. In: Proceedings\n                  of TACAS\u201910, vol. 6015. LNCS, pp. 296\u2013311. Springer, Berlin\n                  (2010)","DOI":"10.1007\/978-3-642-12002-2_25"},{"key":"415_CR14","doi-asserted-by":"crossref","unstructured":"Emmi, M., Jhala, R., Kohler, E., Majumdar, R.: Verifying reference\n                  counting implementations. In: Proceedings of TACAS\u201909. LNCS, vol. 5505, pp.\n                  352\u2013367. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-00768-2_30"},{"issue":"2","key":"415_CR15","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\n                  multithreaded programs. Sci. Comput. Program. 71(2), 89\u2013109 (2008)","journal-title":"Sci. Comput. Program."},{"key":"415_CR16","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.:\n                  Forest automata for verification of heap manipulation. In: Formal Methods in\n                  System Design, pp. 1\u201324 (2012)","DOI":"10.1007\/s10703-012-0150-8"},{"issue":"3","key":"415_CR17","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\n                  for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"415_CR18","unstructured":"IBM. System\/370 principles of operation (1983)"},{"issue":"6","key":"415_CR19","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\n                  concurrency-related bugs using random isolation. STTT 13(6), 495\u2013518 (2011)","journal-title":"STTT"},{"key":"415_CR20","unstructured":"Michael, M., Scott, M.: Correction of a memory management method\n                  for lock-free data structures. Technical Report TR599, University of Rochester,\n                  Rochester (1995)"},{"key":"415_CR21","doi-asserted-by":"crossref","unstructured":"Michael, M., Scott, M.: Simple, fast, and practical non-blocking\n                  and blocking concurrent queue algorithms. In: Proceedings of 15th ACM Symposium on\n                  Principles of Distributed Computing, pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"415_CR22","doi-asserted-by":"crossref","unstructured":"Michael, M.M.: Safe memory reclamation for dynamic lock-free\n                  objects using atomic reads and writes. In: Proceedings of the Twenty-First Annual\n                  Symposium on Principles of Distributed Computing, PODC \u201902, pp. 21\u201330. ACM, New\n                  York (2002)","DOI":"10.1145\/571825.571829"},{"key":"415_CR23","doi-asserted-by":"crossref","unstructured":"Naik, M., Aiken, A., Whaley, J.: Effective static race detection\n                  for java. In: Proceedings of PLDI\u201906, pp. 308\u2013319. ACM, New York\n                  (2006)","DOI":"10.1145\/1133255.1134018"},{"key":"415_CR24","doi-asserted-by":"crossref","unstructured":"Naik, M., Park, C.-S., Sen, K., Gay, D.: Effective static deadlock\n                  detection. In: Proceedings of ICSE, pp. 386\u2013396. IEEE, New York\n                  (2009)","DOI":"10.1109\/ICSE.2009.5070538"},{"key":"415_CR25","doi-asserted-by":"crossref","unstructured":"Segalov, M., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.:\n                  Abstract transformers for thread correlation analysis. In: APLAS, LNCS, pp. 30\u201346.\n                  Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-10672-9_5"},{"key":"415_CR26","unstructured":"Shacham, O.: Verifying atomicity of composed concurrent operations.\n                  PhD thesis, Department of Computer Science, Tel Aviv University\n                  (2012)"},{"key":"415_CR27","unstructured":"Treiber, R.: Systems programming: coping with parallelism.\n                  Technical Report RJ5118, IBM Almaden Res. Ctr. (1986)"},{"key":"415_CR28","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying\n                  linearizability. In: Proceedings of VMCAI, vol. 5403. LNCS, pp. 335\u2013348. Springer,\n                  Berlin (2009)","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"415_CR29","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: CAV, vol.\n                  6174. Lecture Notes in Computer Science, pp. 450\u2013464. Springer, Berlin\n                  (2010)","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"415_CR30","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Rgsep action inference. In: Proceedings of VMCAI\u201910,\n                  vol. 5944. LNCS, pp. 345\u2013361. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-11319-2_25"},{"key":"415_CR31","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to\n                  automatic program verification. In: Proceedings of LICS\u201986, pp. 332\u2013344\n                  (1986)"},{"key":"415_CR32","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E.: Deriving linearizable fine-grained\n                  concurrent objects. In: Proceedings of PLDI\u201908, pp. 125\u2013135. ACM, New York\n                  (2008)","DOI":"10.1145\/1379022.1375598"},{"key":"415_CR33","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking\n                  linearizability. In: Proceedings of SPIN\u201909, vol. 5578. LNCS, pp. 261\u2013278.\n                  Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02652-2_21"},{"key":"415_CR34","doi-asserted-by":"crossref","unstructured":"Wang, L., Stoller, S.: Static analysis of atomicity for programs\n                  with non-blocking synchronization. In: Proceedings of PPOPP\u201905, pp. 61\u201371. ACM,\n                  New York (2005)","DOI":"10.1145\/1065944.1065953"},{"key":"415_CR35","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Expressing interesting properties of programs in\n                  propositional temporal logic (extended abstract). In: Proceedings of POPL\u201986, pp.\n                  184\u2013193 (1986)","DOI":"10.1145\/512644.512661"},{"key":"415_CR36","doi-asserted-by":"crossref","unstructured":"Yahav, E., Sagiv, S.: Automatically verifying concurrent queue\n                  algorithms. Electr. Notes Theor. Comput. Sci. 89(3) (2003)","DOI":"10.1016\/S1571-0661(05)80006-4"}],"updated-by":[{"DOI":"10.1007\/s10009-021-00629-9","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2021,5,31]],"date-time":"2021-05-31T00:00:00Z","timestamp":1622419200000}}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-016-0415-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0415-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0415-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0415-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T04:28:22Z","timestamp":1623990502000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-016-0415-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,16]]},"references-count":36,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["415"],"URL":"https:\/\/doi.org\/10.1007\/s10009-016-0415-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,16]]},"assertion":[{"value":"16 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 May 2021","order":2,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":4,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s10009-021-00629-9","URL":"https:\/\/doi.org\/10.1007\/s10009-021-00629-9","order":5,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}