{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:18Z","timestamp":1776305058065,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540374060","type":"print"},{"value":"9783540374114","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_44","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T05:07:51Z","timestamp":1154754471000},"page":"475-488","source":"Crossref","is-referenced-by-count":57,"title":["Formal Verification of a Lazy Concurrent List-Based Set Algorithm"],"prefix":"10.1007","author":[{"given":"Robert","family":"Colvin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Luchangco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Moir","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"44_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","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, W., Shavit, N.: A lazy concurrent list-based set algorithm. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol.\u00a03974, pp. 3\u201316. Springer, Heidelberg (2006)"},{"issue":"3","key":"44_CR2","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M.P. Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. TOPLAS\u00a012(3), 463\u2013492 (1990)","journal-title":"TOPLAS"},{"key":"44_CR3","unstructured":"Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. In: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida (1995)"},{"key":"44_CR4","unstructured":"Doherty, S.: Modelling and verifying non-blocking algorithms that use dynamically allocated memory. Master\u2019s thesis, School of Mathematical and Computing Sciences, Victoria University of Wellington (2003)"},{"key":"44_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"S. Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol.\u00a03235, pp. 97\u2013114. Springer, Heidelberg (2004)"},{"key":"44_CR6","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proc. Refinement Workshop 2005 (REFINE 2005)","author":"R. Colvin","year":"2005","unstructured":"Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. In: Boiten, E., Derrick, J. (eds.) Proc. Refinement Workshop 2005 (REFINE 2005), Guildford, UK. Electronic Notes in Theoretical Computer Science, vol.\u00a0137(2). Elsevier, Amsterdam (2005)"},{"key":"44_CR7","doi-asserted-by":"crossref","unstructured":"Colvin, R., Groves, L.: Formal verification of an array-based nonblocking queue. In: ICECCS 2005: Proceedings of the 10th IEEE International Conference on Engineering of Complex Computer Systems, Shanghai, Chin, pp. 507\u2013516 (2005)","DOI":"10.1109\/ICECCS.2005.49"},{"issue":"3","key":"44_CR8","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An Introduction to Input\/Output automata. CWI-Quarterly\u00a02(3), 219\u2013246 (1989)","journal-title":"CWI-Quarterly"},{"key":"44_CR9","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)"},{"issue":"2","key":"44_CR10","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N.A. Lynch","year":"1995","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations \u2013 part I: Untimed systems. Information and Computation\u00a0121(2), 214\u2013233 (1995)","journal-title":"Information and Computation"},{"issue":"5","key":"44_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"44_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 496\u2013500. Springer, Heidelberg (2004)"},{"key":"44_CR13","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/1122971.1122992","volume-title":"PPoPP 2006: Proc. 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming","author":"V. Vafeiadis","year":"2006","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP 2006: Proc. 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 129\u2013136. ACM Press, New York (2006)"},{"key":"44_CR14","series-title":"FIP Congress Series, IFIP","first-page":"321","volume-title":"9th IFIP World Computer Congress (Information Processing 1983)","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: 9th IFIP World Computer Congress (Information Processing 1983). FIP Congress Series, IFIP, vol.\u00a09, pp. 321\u2013332. North-Holland, Amsterdam (1983)"},{"issue":"2","key":"44_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q. Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing\u00a09(2), 149\u2013174 (1997)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T19:48:38Z","timestamp":1587152918000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11817963_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}