{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:13:18Z","timestamp":1725491598674},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540752905"},{"type":"electronic","value":"9783540752929"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75292-9_9","type":"book-chapter","created":{"date-parts":[[2007,9,11]],"date-time":"2007-09-11T10:43:07Z","timestamp":1189507387000},"page":"124-138","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Lock-Freedom Using Well-Founded Orders"],"prefix":"10.1007","author":[{"given":"Robert","family":"Colvin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Colvin, R., Dongol, B.: PVS files for lock-freedom of the Treiber stack, \n                  \n                    http:\/\/www.itee.uq.edu.au\/~nbverif\/Lockfreedom_Proofs\/Treiber\/"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. In: Proceedings of the REFINE 2005 Workshop. Electronic Notes in Theoretical Computer Science, vol.\u00a0137, pp. 93\u2013110 (2005)","DOI":"10.1016\/j.entcs.2005.04.026"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1109\/ICECCS.2005.49","volume-title":"10th International Conference on Engineering of Complex Computer Systems","author":"R. Colvin","year":"2005","unstructured":"Colvin, R., Groves, L.: Formal verification of an array-based nonblocking queue. In: 10th International Conference on Engineering of Complex Computer Systems, pp. 507\u2013516. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"9_CR4","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":"9_CR5","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley Longman Publishing Co., Inc., Redwood City, CA, USA (1988)"},{"key":"9_CR6","first-page":"216","volume-title":"Proceedings of the 16th Annual ACM Symposium on Parallel Algorithms","author":"S. Doherty","year":"2004","unstructured":"Doherty, S., Detlefs, D., Groves, L., Flood, C.H., Luchangco, V., Martin, P.A., Moir, M., Shavit, N., Steele, Jr., G.L.: DCAS is not a silver bullet for nonblocking algorithm design. In: Gibbons, P., Adler, M. (eds.) Proceedings of the 16th Annual ACM Symposium on Parallel Algorithms, pp. 216\u2013224. ACM Press, New York (2004)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/11783596_11","volume-title":"Mathematics of Program Construction","author":"B. Dongol","year":"2006","unstructured":"Dongol, B., Mooij, A.J.: Progress in deriving concurrent programs: Emphasizing the role of stable guards. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 140\u2013161. Springer, Heidelberg (2006)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Dongol, B., Mooij, A.J.: Streamlining progress-based derivations of concurrent programs. Formal Aspects of Computing (to appear)","DOI":"10.1007\/s00165-007-0037-4"},{"key":"9_CR10","unstructured":"Doherty, S.: Modelling and verifying non-blocking algorithms that use dynamically allocated memory. Master\u2019s thesis, Victoria University of Wellington (2003)"},{"key":"9_CR11","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., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 284\u2013303. Springer, Heidelberg (2006)"},{"key":"9_CR12","unstructured":"Dongol, B.: Towards simpler proofs of lock-freedom. In: AWCVS\u201906. 1st International Workshop - Asian Working Conference on Verified Software, October 2006, pp. 136\u2013147 (2006)"},{"issue":"3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1093\/logcom\/6.3.343","volume":"6","author":"L. Fix","year":"1996","unstructured":"Fix, L., Grumberg, O.: Verification of temporal properties. J. Log. Comput.\u00a06(3), 343\u2013361 (1996)","journal-title":"J. Log. Comput."},{"issue":"2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/j.ic.2006.10.003","volume":"205","author":"H. Gao","year":"2007","unstructured":"Gao, H., Hesselink, W.H.: A general lock-free algorithm using compare-and-swap. Inf. Comput.\u00a0205(2), 225\u2013241 (2007)","journal-title":"Inf. Comput."},{"key":"9_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3837-7","volume-title":"A logical approach to discrete math","author":"D. Gries","year":"1993","unstructured":"Gries, D., Schneider, F.B.: A logical approach to discrete math. Springer, New York (1993)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/3-540-36108-1_23","volume-title":"Distributed Computing","author":"M. Herlihy","year":"2002","unstructured":"Herlihy, M., Luchangco, V., Moir, M.: The repeat offender problem: A mechanism for supporting dynamic-sized, lock-free data structures. In: Malkhi, D. (ed.) DISC 2002. LNCS, vol.\u00a02508, pp. 339\u2013353. Springer, Heidelberg (2002)"},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1109\/ICDCS.2003.1203503","volume-title":"23rd IEEE International Conference on Distributed Computing Systems","author":"M. Herlihy","year":"2003","unstructured":"Herlihy, M., Luchangco, V., Moir, M.: Obstruction-free synchronization: Double-ended queues as an example. In: 23rd IEEE International Conference on Distributed Computing Systems, p. 522. IEEE Computer Society Press, Los Alamitos (2003)"},{"issue":"6","key":"9_CR18","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1109\/TPDS.2004.8","volume":"15","author":"M.M. Michael","year":"2004","unstructured":"Michael, M.M.: Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst.\u00a015(6), 491\u2013504 (2004)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"9_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8528-6","volume-title":"A Discipline of Multiprogramming","author":"J. Misra","year":"2001","unstructured":"Misra, J.: A Discipline of Multiprogramming. Springer, Heidelberg (2001)"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Moir, M.: Practical implementations of non-blocking synchronization primitives. In: PODC, pp. 219\u2013228 (August 1997)","DOI":"10.1145\/259380.259442"},{"key":"9_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"Temporal Verification of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive and Concurrent Systems: Specification. Springer, New York (1992)"},{"issue":"1","key":"9_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jpdc.1998.1446","volume":"51","author":"M.M. Michael","year":"1998","unstructured":"Michael, M.M., Scott, M.L.: Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors. J. Parallel Distrib. Comput.\u00a051(1), 1\u201326 (1998)","journal-title":"J. Parallel Distrib. Comput."},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"9_CR24","unstructured":"Treiber, R.K.: Systems programming: Coping with parallelism, Technical Report RJ 5118, IBM Almaden Res. Ctr. (1986)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75292-9_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:59:04Z","timestamp":1619521144000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75292-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540752905","9783540752929"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75292-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}