{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T14:02:01Z","timestamp":1768917721405,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642401831","type":"print"},{"value":"9783642401848","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40184-8_17","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:50:56Z","timestamp":1374544256000},"page":"227-241","source":"Crossref","is-referenced-by-count":20,"title":["Characterizing Progress Properties of Concurrent Objects via Contextual Refinements"],"prefix":"10.1007","author":[{"given":"Hongjin","family":"Liang","sequence":"first","affiliation":[]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Aspnes, J., Herlihy, M.: Wait-free data structures in the asynchronous PRAM model. In: SPAA, pp. 340\u2013349 (1990)","DOI":"10.1145\/97444.97701"},{"key":"17_CR2","unstructured":"Birkedal, L., Sieczkowski, F., Thamsborg, J.: A concurrent logical relation. In: CSL, pp. 107\u2013121 (2012)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/11901433_16","volume-title":"Formal Methods and Software Engineering","author":"B. Dongol","year":"2006","unstructured":"Dongol, B.: Formalising progress properties of non-blocking programs. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 284\u2013303. Springer, Heidelberg (2006)"},{"issue":"51-52","key":"17_CR4","doi-asserted-by":"publisher","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"I. Filipovic","year":"2010","unstructured":"Filipovic, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci.\u00a0411(51-52), 4379\u20134398 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-32940-1_21","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"L. Fossati","year":"2012","unstructured":"Fossati, L., Honda, K., Yoshida, N.: Intensional and extensional characterisation of global progress in the \u03c0-calculus. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 287\u2013301. Springer, Heidelberg (2012)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-642-22012-8_36","volume-title":"Automata, Languages and Programming","author":"A. Gotsman","year":"2011","unstructured":"Gotsman, A., Yang, H.: Liveness-preserving atomicity abstraction. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 453\u2013465. Springer, Heidelberg (2011)"},{"issue":"1","key":"17_CR7","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1145\/114005.102808","volume":"13","author":"M. Herlihy","year":"1991","unstructured":"Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst.\u00a013(1), 124\u2013149 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR8","unstructured":"Herlihy, M., Luchangco, V., Moir, M.: Obstruction-free synchronization: Double-ended queues as an example. In: ICDCS, pp. 522\u2013529 (2003)"},{"key":"17_CR9","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (April 2008)"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-25873-2_22","volume-title":"Principles of Distributed Systems","author":"M. Herlihy","year":"2011","unstructured":"Herlihy, M., Shavit, N.: On the nature of progress. In: Fern\u00e0ndez Anta, A., Lipari, G., Roy, M. (eds.) OPODIS 2011. LNCS, vol.\u00a07109, pp. 313\u2013328. Springer, Heidelberg (2011)"},{"issue":"3","key":"17_CR11","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M. Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.: 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":"17_CR12","unstructured":"Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: PLDI (to appear, 2013)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X., Fu, M.: A rely-guarantee-based simulation for verifying concurrent program transformations. In: POPL, pp. 455\u2013468 (2012)","DOI":"10.1145\/2103621.2103711"},{"key":"17_CR14","unstructured":"Liang, H., Hoffmann, J., Feng, X., Shao, Z.: The extended version of the present paper (2013), \n                    \n                      http:\/\/kyhcs.ustcsz.edu.cn\/relconcur\/prog"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Petrank, E., Musuvathi, M., Steensgaard, B.: Progress guarantee for parallel programs via bounded lock-freedom. In: PLDI, pp. 144\u2013154 (2009)","DOI":"10.1145\/1543135.1542493"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2013 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40184-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T02:44:23Z","timestamp":1557974663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40184-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401831","9783642401848"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40184-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}