{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:45:17Z","timestamp":1725727517204},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642391750"},{"type":"electronic","value":"9783642391767"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39176-7_3","type":"book-chapter","created":{"date-parts":[[2013,5,30]],"date-time":"2013-05-30T04:58:44Z","timestamp":1369889924000},"page":"24-42","source":"Crossref","is-referenced-by-count":6,"title":["Verifying a Quantitative Relaxation of Linearizability via Refinement"],"prefix":"10.1007","author":[{"given":"Kiran","family":"Adhikari","sequence":"first","affiliation":[]},{"given":"James","family":"Street","sequence":"additional","affiliation":[]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"ShaoJie","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-642-17653-1_29","volume-title":"Principles of Distributed Systems","author":"Y. Afek","year":"2010","unstructured":"Afek, Y., Korland, G., Yanovsky, E.: Quasi-Linearizability: Relaxed consistency for improved concurrency. In: Lu, C., Masuzawa, T., Mosbah, M. (eds.) OPODIS 2010. LNCS, vol.\u00a06490, pp. 395\u2013410. Springer, Heidelberg (2010)"},{"issue":"5","key":"3_CR2","doi-asserted-by":"publisher","first-page":"1020","DOI":"10.1145\/185675.185815","volume":"41","author":"J. Aspnes","year":"1994","unstructured":"Aspnes, J., Herlihy, M., Shavit, N.: Counting networks. J. ACM\u00a041(5), 1020\u20131048 (1994)","journal-title":"J. ACM"},{"doi-asserted-by":"crossref","unstructured":"Attiya, H., Welch, J.: Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd edn. John Wiley & Sons, Inc., Publication (2004)","key":"3_CR3","DOI":"10.1002\/0471478210"},{"doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: PLDI, pp. 330\u2013340 (2010)","key":"3_CR4","DOI":"10.1145\/1809028.1806634"},{"key":"3_CR5","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":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/11817963_30","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2006","unstructured":"Farzan, A., Madhusudan, P.: Causal atomicity. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 315\u2013328. Springer, Heidelberg (2006)"},{"key":"3_CR7","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.\u00a05123, pp. 52\u201365. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338\u2013349 (2003)","key":"3_CR8","DOI":"10.1145\/780822.781169"},{"unstructured":"Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann (2008)","key":"3_CR9"},{"issue":"3","key":"3_CR10","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":"3_CR11","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-642-33078-0_20","volume-title":"Algorithms and Architectures for Parallel Processing","author":"C.M. Kirsch","year":"2012","unstructured":"Kirsch, C.M., Payer, H., R\u00f6ck, H., Sokolova, A.: Performance, scalability, and semantics of concurrent FIFO queues. In: Xiang, Y., Stojmenovic, I., Apduhan, B.O., Wang, G., Nakano, K., Zomaya, A. (eds.) ICA3PP 2012, Part I. LNCS, vol.\u00a07439, pp. 273\u2013287. Springer, Heidelberg (2012)"},{"issue":"9","key":"3_CR13","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers\u00a028(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Computers"},{"doi-asserted-by":"crossref","unstructured":"Liu, Y., Chen, W., Liu, Y., Zhang, S., Sun, J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE Transactions on Software Engineering (2013)","key":"3_CR14","DOI":"10.1109\/TSE.2012.82"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-05089-3_21","volume-title":"FM 2009: Formal Methods","author":"Y. Liu","year":"2009","unstructured":"Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 321\u2013337. Springer, Heidelberg (2009)"},{"unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann (1997)","key":"3_CR16"},{"doi-asserted-by":"crossref","unstructured":"Payer, H., R\u00f6ck, H., Kirsch, C.M., Sokolova, A.: Scalability versus semantics of concurrent fifo queues. In: PODC, pp. 331\u2013332 (2011)","key":"3_CR17","DOI":"10.1145\/1993806.1993869"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-642-00590-9_28","volume-title":"Programming Languages and Systems","author":"C. Sadowski","year":"2009","unstructured":"Sadowski, C., Freund, S.N., Flanagan, C.: Singletrack: A dynamic determinism checker for multithreaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 394\u2013409. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: TASE, pp. 127\u2013135 (2009)","key":"3_CR19","DOI":"10.1109\/TASE.2009.32"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer, Heidelberg (2009)"},{"unstructured":"Treiber, R.K.: Systems Programming: Coping with Parallelism. Technical Report RJ 5118, IBM Almaden Research Center (1986)","key":"3_CR21"},{"key":"3_CR22","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":"3_CR23","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)"},{"issue":"1","key":"3_CR24","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1435417.1435432","volume":"52","author":"W. Vogels","year":"2009","unstructured":"Vogels, W.: Eventually consistent. Commun. ACM\u00a052(1), 40\u201344 (2009)","journal-title":"Commun. ACM"},{"key":"3_CR25","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.\u00a06015, pp. 328\u2013342. Springer, Heidelberg (2010)"},{"issue":"2","key":"3_CR26","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","volume":"32","author":"L. Wang","year":"2006","unstructured":"Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Software Eng.\u00a032(2), 93\u2013110 (2006)","journal-title":"IEEE Trans. Software Eng."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39176-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T08:53:48Z","timestamp":1557737628000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39176-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642391750","9783642391767"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39176-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}