{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:58:33Z","timestamp":1748350713367},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540688624"},{"type":"electronic","value":"9783540688631"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-68863-1_6","type":"book-chapter","created":{"date-parts":[[2008,6,2]],"date-time":"2008-06-02T07:20:45Z","timestamp":1212391245000},"page":"78-95","source":"Crossref","is-referenced-by-count":11,"title":["Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack"],"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":[{"issue":"5","key":"6_CR1","first-page":"744","volume":"11","author":"J.-R. Abrial","year":"2005","unstructured":"Abrial, J.-R., Cansell, D.: Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity). Journal of Universal Computer Science\u00a011(5), 744\u2013770 (2005)","journal-title":"Journal of Universal Computer Science"},{"key":"6_CR2","series-title":"BCS Practitioner Series","volume-title":"Z in Practice","author":"R. Barden","year":"1994","unstructured":"Barden, R., Stepney, S., Cooper, D.: Z in Practice. BCS Practitioner Series. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"6_CR3","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":"6_CR4","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W. Roever de","year":"1998","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, Cambridge (1998)"},{"key":"6_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0257-1","volume-title":"Refinement in Z and Object-Z: Foundations and Advanced Applications","author":"J. Derrick","year":"2001","unstructured":"Derrick, J., Boiten, E.: Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer, Heidelberg (2001)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-540-73210-5_11","volume-title":"Integrated Formal Methods","author":"J. Derrick","year":"2007","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Proving linearizability via non-atomic refinement. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 195\u2013214. Springer, Heidelberg (2007)"},{"key":"6_CR7","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., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 127\u2013147. Springer, Heidelberg (2003)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","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., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, Springer, Heidelberg (2005)"},{"key":"6_CR9","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)"},{"doi-asserted-by":"crossref","unstructured":"Groves, L., Colvin, R.: Derivation of a scalable lock-free stack algorithm. ENTCS (to appear, 2007)","key":"6_CR10","DOI":"10.1016\/j.entcs.2006.08.044"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","first-page":"187","volume-title":"ESOP 1986","author":"H. Jifeng","year":"1986","unstructured":"Jifeng, H., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol.\u00a0213, pp. 187\u2013196. Springer, Heidelberg (1986)"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1145\/1007912.1007944","volume-title":"SPAA 2004: ACM symposium on Parallelism in algorithms and architectures","author":"D. Hendler","year":"2004","unstructured":"Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. In: SPAA 2004: ACM symposium on Parallelism in algorithms and architectures, pp. 206\u2013215. ACM Press, New York (2004)"},{"issue":"3","key":"6_CR13","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 Transactions on Programming Languages and Systems\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"6_CR14","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s00236-006-0020-1","volume":"43","author":"W.H. Hesselink","year":"2006","unstructured":"Hesselink, W.H.: Refinement verification of the lazy caching algorithm. Acta Inf.\u00a043(3), 195\u2013222 (2006)","journal-title":"Acta Inf."},{"issue":"2","key":"6_CR15","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s00236-007-0044-1","volume":"44","author":"W.H. Hesselink","year":"2007","unstructured":"Hesselink, W.H.: A criterion for atomicity revisited. Acta Inf.\u00a044(2), 123\u2013151 (2007)","journal-title":"Acta Inf."},{"unstructured":"Web presentation of the linearization case study in KIV. URL: \n                      \n                        http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/linearizability.html","key":"6_CR16"},{"unstructured":"Lamport, L., Schneider, F.B.: Pretending atomicity. Technical Report TR89-1005, SRC Digital (1989)","key":"6_CR17"},{"issue":"12","key":"6_CR18","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R.J. Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM\u00a018(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"issue":"1","key":"6_CR19","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 \u2014 memory multiprocessors. Journal of Parallel and Distributed Computing\u00a051(1), 1\u201326 (1998)","journal-title":"Journal of Parallel and Distributed Computing"},{"key":"6_CR20","series-title":"Systems and Implementation Techniques","doi-asserted-by":"crossref","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 (ch. 1: Interactive Theorem Proving). In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications. Systems and Implementation Techniques, vol.\u00a0II, pp. 13\u201339. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"6_CR21","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"6_CR22","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J.C.P. Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Open Object-Based Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68863-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,2]],"date-time":"2019-03-02T07:44:20Z","timestamp":1551512660000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68863-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540688624","9783540688631"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68863-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}