{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:59:16Z","timestamp":1748350756366},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214363"},{"type":"electronic","value":"9783642214370"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_25","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T07:33:16Z","timestamp":1308382396000},"page":"323-337","source":"Crossref","is-referenced-by-count":20,"title":["Verifying Linearisability with Potential Linearisation Points"],"prefix":"10.1007","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","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.W., 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)"},{"key":"25_CR2","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":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/11817963_44","volume-title":"Computer Aided Verification","author":"R. Colvin","year":"2006","unstructured":"Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set algorithm. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 475\u2013488. Springer, Heidelberg (2006)"},{"key":"25_CR4","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":"25_CR5","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":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/11415787_3","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"J. Derrick","year":"2005","unstructured":"Derrick, J., Wehrheim, H.: Non-atomic refinement in Z and CSP. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, pp. 24\u201344. Springer, Heidelberg (2005)"},{"issue":"51-52","key":"25_CR7","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.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theoretical Computer Science\u00a0411(51-52), 4379\u20134398 (2010)","journal-title":"Theoretical Computer Science"},{"issue":"1\u20132","key":"25_CR8","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s00165-008-0092-5","volume":"21","author":"L. Groves","year":"2009","unstructured":"Groves, L., Colvin, R.: Trace-based derivation of a scalable lock-free stack algorithm. Formal Aspects of Computing (FAC)\u00a021(1\u20132), 187\u2013223 (2009)","journal-title":"Formal Aspects of Computing (FAC)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/11795490_3","volume-title":"Principles of Distributed Systems","author":"S. Heller","year":"2006","unstructured":"Heller, S., Herlihy, M., Luchangco, V., Moir, M., Scherer III, W.N., Shavit, N.: A lazy concurrent list-based set algorithm. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol.\u00a03974, pp. 305\u2013309. Springer, Heidelberg (2006)"},{"key":"25_CR10","first-page":"206","volume-title":"SPAA 2004","author":"D. Hendler","year":"2004","unstructured":"Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. In: SPAA 2004, pp. 206\u2013215. ACM Press, New York (2004)"},{"issue":"3","key":"25_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.M.: Linearizability: A correctness condition for concurrent objects. ACM TOPLAS\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"key":"25_CR12","unstructured":"Web presentation of linearizability theory and the lazy set algorithm (2010), http:\/\/www.informatik.uniaugsburg.de\/swt\/projects\/possibilities.html"},{"key":"25_CR13","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)"},{"key":"25_CR14","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann Publishers, San Francisco (1996)"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proc. 15th ACM Symp. on Principles of Distributed Computing, pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: 29th Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), pp. 85\u201394 (2010)","DOI":"10.1145\/1835698.1835722"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-94-017-0435-9_1","volume-title":"Automated Deduction\u2014A Basis for Applications","author":"W. Reif","year":"1998","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, Dordrecht (1998)"},{"key":"25_CR18","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. PhD thesis, University of Cambridge (2007)"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V. Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 450\u2013464. Springer, Heidelberg (2010)"},{"key":"25_CR20","first-page":"129","volume-title":"PPoPP 2006","author":"V. Vafeiadis","year":"2006","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP 2006, pp. 129\u2013136. ACM, New York (2006)"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/Guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T00:07:12Z","timestamp":1560298032000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}