{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T13:44:43Z","timestamp":1760708683850},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319064093"},{"type":"electronic","value":"9783319064109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_15","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"200-214","source":"Crossref","is-referenced-by-count":12,"title":["Quiescent Consistency: Defining and Verifying Relaxed Linearizability"],"prefix":"10.1007","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[]},{"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Bogdan","family":"Tofan","sequence":"additional","affiliation":[]},{"given":"Oleg","family":"Travkin","sequence":"additional","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-15291-7_16","volume-title":"Euro-Par 2010 - Parallel Processing","author":"Y. Afek","year":"2010","unstructured":"Afek, Y., Korland, G., Natanzon, M., Shavit, N.: Scalable producer-consumer pools based on elimination-diffraction trees. In: D\u2019Ambra, P., Guarracino, M., Talia, D. (eds.) Euro-Par 2010, Part II. LNCS, vol.\u00a06272, pp. 151\u2013162. Springer, Heidelberg (2010)"},{"key":"15_CR2","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)"},{"key":"15_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)"},{"issue":"5","key":"15_CR4","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. Journal of the ACM\u00a041(5), 1020\u20131048 (1994)","journal-title":"Journal of the ACM"},{"key":"15_CR5","first-page":"93","volume":"137","author":"R. Colvin","year":"2005","unstructured":"Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. ENTCS\u00a0137, 93\u2013110 (2005)","journal-title":"ENTCS"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"de Roever, W., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol.\u00a047. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Derrick, J., Boiten, E.: Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer (May 2001)","DOI":"10.1007\/978-1-4471-0257-1"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1477","DOI":"10.1007\/3-540-48118-4_28","volume-title":"FM\u201999 - Formal Methods","author":"J. Derrick","year":"1999","unstructured":"Derrick, J., Boiten, E.A.: Non-atomic refinement in Z. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1477\u20131496. Springer, Heidelberg (1999)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-68863-1_6","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"J. Derrick","year":"2008","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanizing a correctness proof for a lock-free concurrent stack. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 78\u201395. Springer, Heidelberg (2008)"},{"issue":"1","key":"15_CR10","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/1889997.1890001","volume":"33","author":"J. Derrick","year":"2011","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst.\u00a033(1), 4 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-44880-2_10","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"J. Derrick","year":"2003","unstructured":"Derrick, J., Wehrheim, H.: Using coupled simulations in non-atomic refinement. In: Bert, D., Bowen, J.P., King, S., Wald\u00e9n, M. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 127\u2013147. Springer, Heidelberg (2003)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kirsch, C.M., Payer, H., Sezgin, A., Sokolova, A.: Quantitative relaxation of concurrent data structures. In: POPL, pp. 317\u2013328. ACM (2013)","DOI":"10.1145\/2480359.2429109"},{"key":"15_CR13","unstructured":"Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann (2008)"},{"issue":"3","key":"15_CR14","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 TOPLAS\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"issue":"9","key":"15_CR15","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"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Automated Deduction\u2014A Basis for Applications, Interactive Theorem Proving, vol.\u00a0II, ch. 1, pp. 13\u201339. Kluwer (1998)","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-31424-7_21","volume-title":"Computer Aided Verification","author":"G. Schellhorn","year":"2012","unstructured":"Schellhorn, G., Wehrheim, H., Derrick, J.: How to prove algorithms linearisable. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 243\u2013259. Springer, Heidelberg (2012)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Shapiro, M., Kemme, B.: Eventual consistency. In: Liu, L., \u00d6zsu, M.T. (eds.) Encyclopedia of Database Systems, pp. 1071\u20131072. Springer US (2009)","DOI":"10.1007\/978-0-387-39940-9_1366"},{"issue":"3","key":"15_CR19","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1897852.1897873","volume":"54","author":"N. Shavit","year":"2011","unstructured":"Shavit, N.: Data structures in the multicore age. Commun. ACM\u00a054(3), 76\u201384 (2011)","journal-title":"Commun. ACM"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-23283-1_16","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2011","author":"B. Tofan","year":"2011","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: Formal verification of a lock-free stack with hazard pointers. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol.\u00a06916, pp. 239\u2013255. Springer, Heidelberg (2011)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP 2006, pp. 129\u2013136. ACM (2006)","DOI":"10.1145\/1122971.1122992"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,18]],"date-time":"2020-08-18T01:48:57Z","timestamp":1597715337000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}