{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T11:49:06Z","timestamp":1783684146931,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642370359","type":"print"},{"value":"9783642370366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37036-6_15","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:35:55Z","timestamp":1361216155000},"page":"249-269","source":"Crossref","is-referenced-by-count":40,"title":["Verifying Concurrent Memory Reclamation Algorithms with Grace"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Gotsman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking Interference with Fractional Permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P., Yang, H.: Local action and abstract separation logic. In: LICS (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL (2009)","DOI":"10.1145\/1594834.1480885"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-71316-6_13","volume-title":"Programming Languages and Systems","author":"X. Feng","year":"2007","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 173\u2013188. Springer, Heidelberg (2007)"},{"key":"15_CR5","unstructured":"Fraser, K.: Practical lock-freedom. PhD Thesis. University of Cambridge (2004)"},{"key":"15_CR6","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":"15_CR7","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Rinetzky, N., Yang, H.: Verifying concurrent memory reclamation algorithms with grace. Technical Report 7\/13, School of Computer Science, Tel-Aviv University (2013), \n                    \n                      http:\/\/www.cs.tau.ac.il\/~maon","DOI":"10.1007\/978-3-642-37036-6_15"},{"key":"15_CR8","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":"15_CR9","doi-asserted-by":"crossref","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. TOPLAS (1990)","DOI":"10.1145\/78969.78972"},{"key":"15_CR10","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress (1983)"},{"key":"15_CR11","unstructured":"McKenney, P.: Exploiting deferred destruction: an analysis of read-copy-update techniques in operating system kernels. PhD Thesis. OGI (2004)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Michael, M.M.: Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst. (2004)","DOI":"10.1109\/TPDS.2004.8"},{"key":"15_CR13","unstructured":"O\u2019Hearn, P.: Resources, concurrency and local reasoning. TCS (2007)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bornat, R., O\u2019Hearn, P.: Modular verification of a non-blocking stack. In: POPL (2007)","DOI":"10.1145\/1190216.1190261"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-23283-1_16","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2011","author":"B. Tofan","year":"2011","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: Formal Verification of a Lock-Free Stack with Hazard Pointers. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol.\u00a06916, pp. 239\u2013255. Springer, Heidelberg (2011)"},{"key":"15_CR17","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. PhD Thesis. University of Cambridge (2008)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37036-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T08:23:59Z","timestamp":1557563039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37036-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370359","9783642370366"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37036-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}