{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T11:37:22Z","timestamp":1761824242545,"version":"3.40.3"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030532871"},{"type":"electronic","value":"9783030532888"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53288-8_17","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T19:03:27Z","timestamp":1594839807000},"page":"350-375","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Root Causing Linearizability Violations"],"prefix":"10.1007","author":[{"given":"Berk","family":"\u00c7irisci","sequence":"first","affiliation":[]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[]},{"given":"Azadeh","family":"Farzan","sequence":"additional","affiliation":[]},{"given":"Suha Orhun","family":"Mutluergil","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"issue":"4","key":"17_CR1","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s00446-007-0023-3","volume":"20","author":"Y Afek","year":"2007","unstructured":"Afek, Y., Gafni, E., Morrison, A.: Common2 extended to stacks and unbounded concurrency. Distrib. Comput. 20(4), 239\u2013252 (2007). \nhttps:\/\/doi.org\/10.1007\/s00446-007-0023-3","journal-title":"Distrib. Comput."},{"key":"17_CR2","doi-asserted-by":"publisher","unstructured":"Bloem, R., Hofferek, G., K\u00f6nighofer, B., K\u00f6nighofer, R., Ausserlechner, S., Spork, R.: Synthesis of synchronization using uninterpreted functions. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 October 2014, pp. 35\u201342. IEEE (2014). \nhttps:\/\/doi.org\/10.1109\/FMCAD.2014.6987593","DOI":"10.1109\/FMCAD.2014.6987593"},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15\u201317 January 2015, pp. 651\u2013662. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2676726.2677002","DOI":"10.1145\/2676726.2677002"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Zorn, B.G., Aiken, A. (eds.) Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, 5\u201310 June 2010, pp. 330\u2013340. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1806596.1806634","DOI":"10.1145\/1806596.1806634"},{"key":"17_CR5","doi-asserted-by":"publisher","unstructured":"Burnim, J., Necula, G.C., Sen, K.: Specifying and checking semantic atomicity for multithreaded programs. In: Gupta, R., Mowry, T.C. (eds.) Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2011, Newport Beach, CA, USA, 5\u201311 March 2011, pp. 79\u201390. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/1950365.1950377","DOI":"10.1145\/1950365.1950377"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-319-21668-3_11","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2015","unstructured":"\u010cern\u00fd, P., et al.: From non-preemptive to preemptive scheduling using synchronization synthesis. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 180\u2013197. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21668-3_11"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"951","DOI":"10.1007\/978-3-642-39799-8_68","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2013","unstructured":"\u010cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 951\u2013967. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_68"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-319-08867-9_38","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2014","unstructured":"\u010cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Regression-free synthesis for concurrency. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 568\u2013584. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_38"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Cherem, S., Chilimbi, T.M., Gulwani, S.: Inferring locks for atomic sections. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7\u201313 June 2008, pp. 304\u2013315. ACM (2008). \nhttps:\/\/doi.org\/10.1145\/1375581.1375619","DOI":"10.1145\/1375581.1375619"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Chew, L., Lie, D.: Kivati: fast detection and prevention of atomicity violations. In: Morin, C., Muller, G. (eds.) European Conference on Computer Systems, Proceedings of the 5th European Conference on Computer Systems, EuroSys 2010, Paris, France, 13\u201316 April 2010, pp. 307\u2013320. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1755913.1755945","DOI":"10.1145\/1755913.1755945"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-69850-0_12","volume-title":"25 Years of Model Checking","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 196\u2013215. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-69850-0_12"},{"key":"17_CR12","unstructured":"Emmi, M., Enea, C.: Exposing non-atomic methods of concurrent objects. CoRR abs\/1706.09305 (2017). \nhttp:\/\/arxiv.org\/abs\/1706.09305"},{"key":"17_CR13","doi-asserted-by":"publisher","unstructured":"Emmi, M., Enea, C.: Sound, complete, and tractable linearizability monitoring for concurrent collections. PACMPL 2(POPL), 25:1\u201325:27 (2018). \nhttps:\/\/doi.org\/10.1145\/3158113","DOI":"10.1145\/3158113"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/978-3-030-25543-5_30","volume-title":"Computer Aided Verification","author":"M Emmi","year":"2019","unstructured":"Emmi, M., Enea, C.: Violat: generating tests of observational refinement for concurrent objects. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 534\u2013546. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-25543-5_30"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Emmi, M., Enea, C.: Weak-consistency specification via visibility relaxation. PACMPL 3(POPL), 60:1\u201360:28 (2019). \nhttps:\/\/doi.org\/10.1145\/3290373","DOI":"10.1145\/3290373"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Emmi, M., Enea, C., Hamza, J.: Monitoring refinement via symbolic reasoning. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15\u201317 June 2015, pp. 260\u2013269. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2737924.2737983","DOI":"10.1145\/2737924.2737983"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"Emmi, M., Fischer, J.S., Jhala, R., Majumdar, R.: Lock allocation. In: Hofmann, M., Felleisen, M. (eds.) Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, 17\u201319 January 2007, pp. 291\u2013296. ACM (2007). \nhttps:\/\/doi.org\/10.1145\/1190216.1190260","DOI":"10.1145\/1190216.1190260"},{"key":"17_CR18","doi-asserted-by":"publisher","unstructured":"Engler, D.R., Ashcraft, K.: Racerx: effective, static detection of race conditions and deadlocks. In: Scott, M.L., Peterson, L.L. (eds.) Proceedings of the 19th ACM Symposium on Operating Systems Principles 2003, SOSP 2003, Bolton Landing, NY, USA, 19\u201322 October 2003, pp. 237\u2013252. ACM (2003). \nhttps:\/\/doi.org\/10.1145\/945445.945468","DOI":"10.1145\/945445.945468"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-70545-1_8","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2008","unstructured":"Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 52\u201365. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-70545-1_8"},{"issue":"4","key":"17_CR20","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"PB Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997). \nhttps:\/\/doi.org\/10.1137\/S0097539794279614","journal-title":"SIAM J. Comput."},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Gramoli, V.: More than you ever wanted to know about synchronization: synchrobench, measuring the impact of the synchronization on concurrent algorithms. In: Cohen, A., Grove, D. (eds.) Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2015, San Francisco, CA, USA, 7\u201311 February 2015, pp. 1\u201310. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2688500.2688501","DOI":"10.1145\/2688500.2688501"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Gupta, A., Henzinger, T.A., Radhakrishna, A., Samanta, R., Tarrach, T.: Succinct representation of concurrent trace sets. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15\u201317 January 2015, pp. 433\u2013444. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2676726.2677008","DOI":"10.1145\/2676726.2677008"},{"key":"17_CR23","volume-title":"The Art of Multiprocessor Programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, Burlington (2008)"},{"issue":"3","key":"17_CR24","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. 12(3), 463\u2013492 (1990). \nhttps:\/\/doi.org\/10.1145\/78969.78972","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-19195-9_4","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"A Horn","year":"2015","unstructured":"Horn, A., Kroening, D.: Faster linearizability checking via P-compositionality. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 50\u201365. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19195-9_4"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-23702-7_15","volume-title":"Static Analysis","author":"J Huang","year":"2011","unstructured":"Huang, J., Zhang, C.: An efficient static trace simplification technique for debugging concurrent programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 163\u2013179. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-23702-7_15"},{"key":"17_CR27","doi-asserted-by":"publisher","unstructured":"Jalbert, N., Sen, K.: A trace simplification technique for effective debugging of concurrent programs. In: Roman, G., van der Hoek, A. (eds.) Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010, Santa Fe, NM, USA, 7\u201311 November 2010, pp. 57\u201366. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1882291.1882302","DOI":"10.1145\/1882291.1882302"},{"key":"17_CR28","doi-asserted-by":"publisher","unstructured":"Jin, G., Song, L., Zhang, W., Lu, S., Liblit, B.: Automated atomicity-violation fixing. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, 4\u20138 June 2011, pp. 389\u2013400. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/1993498.1993544","DOI":"10.1145\/1993498.1993544"},{"key":"17_CR29","unstructured":"Jin, G., Zhang, W., Deng, D.: Automated concurrency-bug fixing. In: Thekkath, C., Vahdat, A. (eds.) 10th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2012, Hollywood, CA, USA, 8\u201310 October 2012, pp. 221\u2013236. USENIX Association (2012). \nhttps:\/\/www.usenix.org\/conference\/osdi12\/technical-sessions\/presentation\/jin"},{"key":"17_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-70545-1_47","volume-title":"Computer Aided Verification","author":"S Kashyap","year":"2008","unstructured":"Kashyap, S., Garg, V.K.: Producing short counterexamples using \u201ccrucial events\u201d. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 491\u2013503. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-70545-1_47"},{"issue":"4","key":"17_CR31","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1145\/942572.807045","volume":"9","author":"B Liskov","year":"1974","unstructured":"Liskov, B., Zilles, S.N.: Programming with abstract data types. SIGPLAN Not. 9(4), 50\u201359 (1974)","journal-title":"SIGPLAN Not."},{"key":"17_CR32","doi-asserted-by":"publisher","unstructured":"Liu, P., Tripp, O., Zhang, X.: Flint: fixing linearizability violations. In: Black, A.P., Millstein, T.D. (eds.) Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, 20\u201324 October 2014, pp. 543\u2013560. ACM (2014). \nhttps:\/\/doi.org\/10.1145\/2660193.2660217","DOI":"10.1145\/2660193.2660217"},{"key":"17_CR33","doi-asserted-by":"publisher","unstructured":"Lowe, G.: Testing for linearizability. Concurr. Comput.: Pract. Exper. 29(4) (2017). \nhttps:\/\/doi.org\/10.1002\/cpe.3928","DOI":"10.1002\/cpe.3928"},{"issue":"1","key":"17_CR34","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6(1), 68\u201393 (1984). \nhttps:\/\/doi.org\/10.1145\/357233.357237","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR35","unstructured":"Michael, M.M.: ABA prevention using single-word instructions. Technical report RC 23089, IBM Thomas J. Watson Research Center, January 2004"},{"key":"17_CR36","doi-asserted-by":"publisher","unstructured":"Moir, M., Shavit, N.: Concurrent data structures. In: Mehta, D.P., Sahni, S. (eds.) Handbook of Data Structures and Applications. Chapman and Hall\/CRC (2004). \nhttps:\/\/doi.org\/10.1201\/9781420035179.ch47","DOI":"10.1201\/9781420035179.ch47"},{"issue":"4","key":"17_CR37","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"CH Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM 26(4), 631\u2013653 (1979). \nhttps:\/\/doi.org\/10.1145\/322154.322158","journal-title":"J. ACM"},{"key":"17_CR38","doi-asserted-by":"publisher","unstructured":"Park, S., Lu, S., Zhou, Y.: Ctrigger: exposing atomicity violation bugs from their hiding places. In: Soffa, M.L., Irwin, M.J. (eds.) Proceedings of the 14th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2009, Washington, DC, USA, 7\u201311 March 2009, pp. 25\u201336. ACM (2009). \nhttps:\/\/doi.org\/10.1145\/1508244.1508249","DOI":"10.1145\/1508244.1508249"},{"key":"17_CR39","doi-asserted-by":"publisher","unstructured":"Pradel, M., Gross, T.R.: Automatic testing of sequential and concurrent substitutability. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) 35th International Conference on Software Engineering, ICSE 2013, San Francisco, CA, USA, 18\u201326 May 2013, pp. 282\u2013291. IEEE Computer Society (2013). \nhttps:\/\/doi.org\/10.1109\/ICSE.2013.6606574","DOI":"10.1109\/ICSE.2013.6606574"},{"key":"17_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-20398-5_23","volume-title":"NASA Formal Methods","author":"M Said","year":"2011","unstructured":"Said, M., Wang, C., Yang, Z., Sakallah, K.: Generating data race witnesses by an SMT-based analysis. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 313\u2013327. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-20398-5_23"},{"issue":"4","key":"17_CR41","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391\u2013411 (1997). \nhttps:\/\/doi.org\/10.1145\/265924.265927","journal-title":"ACM Trans. Comput. Syst."},{"key":"17_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-00768-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 139\u2013154. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-00768-2_13"},{"key":"17_CR43","doi-asserted-by":"publisher","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17\u201323 January 2010, pp. 327\u2013338. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1706299.1706338","DOI":"10.1145\/1706299.1706338"},{"key":"17_CR44","doi-asserted-by":"publisher","unstructured":"Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with java pathfinder. In: Avrunin, G.S., Rothermel, G. (eds.) Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, 11\u201314 July 2004, pp. 97\u2013107. ACM (2004). \nhttps:\/\/doi.org\/10.1145\/1007512.1007526","DOI":"10.1145\/1007512.1007526"},{"key":"17_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-12002-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Wang","year":"2010","unstructured":"Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 328\u2013342. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-12002-2_27"},{"key":"17_CR46","doi-asserted-by":"publisher","unstructured":"Weeratunge, D., Zhang, X., Jagannathan, S.: Accentuating the positive: atomicity inference and enforcement using correct executions. In: Lopes, C.V., Fisher, K. (eds.) Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, 22\u201327 October 2011, pp. 19\u201334. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/2048066.2048071","DOI":"10.1145\/2048066.2048071"},{"issue":"1\u20132","key":"17_CR47","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1006\/jpdc.1993.1015","volume":"17","author":"JM Wing","year":"1993","unstructured":"Wing, J.M., Gong, C.: Testing and verifying concurrent objects. J. Parallel Distrib. Comput. 17(1\u20132), 164\u2013182 (1993). \nhttps:\/\/doi.org\/10.1006\/jpdc.1993.1015","journal-title":"J. Parallel Distrib. Comput."},{"key":"17_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-89740-8_10","volume-title":"Languages and Compilers for Parallel Computing","author":"Y Zhang","year":"2008","unstructured":"Zhang, Y., Sreedhar, V.C., Zhu, W., Sarkar, V., Gao, G.R.: Minimum lock assignment: a method for exploiting concurrency among critical sections. In: Amaral, J.N. (ed.) LCPC 2008. LNCS, vol. 5335, pp. 141\u2013155. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-89740-8_10"}],"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-030-53288-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T19:08:57Z","timestamp":1594840137000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53288-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532871","9783030532888"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53288-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}