{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:32:05Z","timestamp":1752985925954,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642232824"},{"type":"electronic","value":"9783642232831"}],"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-23283-1_16","type":"book-chapter","created":{"date-parts":[[2011,8,24]],"date-time":"2011-08-24T02:30:27Z","timestamp":1314153027000},"page":"239-255","source":"Crossref","is-referenced-by-count":14,"title":["Formal Verification of a Lock-Free Stack with Hazard Pointers"],"prefix":"10.1007","author":[{"given":"Bogdan","family":"Tofan","sequence":"first","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Massalin, H., Pu, C.: A lock-free multiprocessor os kernel. Technical Report CUCS-005-91, Columbia University (1991)"},{"issue":"3","key":"16_CR2","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. on Prog. Languages and Systems\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Trans. on Prog. Languages and Systems"},{"key":"16_CR3","unstructured":"Treiber, R.K.: System programming: Coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center (1986)"},{"issue":"6","key":"16_CR4","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."},{"issue":"1","key":"16_CR5","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1145\/1190215.1190261","volume":"42","author":"M. Parkinson","year":"2007","unstructured":"Parkinson, M., Bornat, R., O\u2019Hearn, P.: Modular verification of a non-blocking stack. SIGPLAN Not.\u00a042(1), 297\u2013302 (2007)","journal-title":"SIGPLAN Not."},{"key":"16_CR6","series-title":"Systems and Implementation Techniques","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: 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":"16_CR7","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: Verifying a stack with hazard pointers in temporal logic. Technical Report 2011-08, Universit\u00e4t Augsburg (2011), http:\/\/opus.bibliothek.uni-augsburg.de\/volltexte\/2011\/1717\/"},{"key":"16_CR8","unstructured":"KIV. Presentation of proofs for concurrent algorithms (2011), http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/lock-free.html"},{"key":"16_CR9","volume-title":"Executing Temporal Logic Programs","author":"B. Moszkowski","year":"1986","unstructured":"Moszkowski, B.: Executing Temporal Logic Programs. Cambr. Univ. Press, Cambridge (1986)"},{"key":"16_CR10","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods","author":"W.P. Roever de","year":"2001","unstructured":"de Roever, W.P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol.\u00a054. Cambridge University Press, Cambridge (2001)"},{"key":"16_CR11","first-page":"309","volume":"74","author":"R.M. Burstall","year":"1974","unstructured":"Burstall, R.M.: Program proving as hand simulation with a little induction. Information Processing\u00a074, 309\u2013312 (1974)","journal-title":"Information Processing"},{"issue":"2,3","key":"16_CR12","doi-asserted-by":"crossref","first-page":"285","DOI":"10.3233\/AIC-2010-0458","volume":"23","author":"S. B\u00e4umler","year":"2010","unstructured":"B\u00e4umler, S., Balser, M., Nafz, F., Reif, W., Schellhorn, G.: Interactive verification of concurrent systems using symbolic execution. AI Communications\u00a023(2,3), 285\u2013307 (2010)","journal-title":"AI Communications"},{"key":"16_CR13","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Reif, W.: Interleaved programs and rely-guarantee reasoning with ITL. In: Proc. of TIME. IEEE, CPS (to appear, 2011)"},{"key":"16_CR14","unstructured":"B\u00e4umler, S., Schellhorn, G., Tofan, B., Reif, W.: Proving linearizability with temporal logic. In: Formal Aspects of Computing (FAC) (2009), appeared online first http:\/\/www.springerlink.com\/content\/7507m59834066h04\/"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-13321-3_21","volume-title":"Mathematics of Program Construction","author":"B. Tofan","year":"2010","unstructured":"Tofan, B., B\u00e4umler, S., Schellhorn, G., Reif, W.: Temporal logic verification of lock-freedom. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol.\u00a06120, pp. 377\u2013396. Springer, Heidelberg (2010)"},{"key":"16_CR16","first-page":"321","volume-title":"Proceedings of IFIP 1983","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP 1983, pp. 321\u2013332. North-Holland, Amsterdam (1983)"},{"key":"16_CR17","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\u00a0practical 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":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-15375-4_27","volume-title":"CONCUR 2010 - Concurrency Theory","author":"M. Fu","year":"2010","unstructured":"Fu, M., Li, Y., Feng, X., Shao, Z., Zhang, Y.: Reasoning about optimistic concurrency using a program logic for history. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 388\u2013402. Springer, Heidelberg (2010)"},{"key":"16_CR19","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Verifying linearisabilty with potential linearisation points. In: Proc. Formal Methods (to appear, 2011)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2011"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23283-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,22]],"date-time":"2020-06-22T15:41:22Z","timestamp":1592840482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23283-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642232824","9783642232831"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23283-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}