{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T19:03:01Z","timestamp":1742929381430,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031659409"},{"type":"electronic","value":"9783031659416"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-65941-6_3","type":"book-chapter","created":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:10:56Z","timestamp":1722496256000},"page":"45-61","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Safe Memory Reclamation in\u00a0Concurrent Programs with\u00a0CafeOBJ"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7092-2084","authenticated-orcid":false,"given":"Duong Dinh","family":"Tran","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,2]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Astesiano, E., Kreowski, H., Krieg-Br\u00fcckner, B. (eds.): Algebraic Foundations of Systems Specification. IFIP State-of-the-Art Reports. Springer, Berlin (1999). https:\/\/doi.org\/10.1007\/978-3-642-59851-7","DOI":"10.1007\/978-3-642-59851-7"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1\u20133), 227\u2013270 (2007). https:\/\/doi.org\/10.1016\/J.TCS.2006.12.034","DOI":"10.1016\/J.TCS.2006.12.034"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude, Lecture Notes in Computer Science, vol.\u00a04350. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. J. Univers. Comput. Sci. 12(11), 1618\u20131650 (2006). https:\/\/doi.org\/10.3217\/JUCS-012-11-1618","DOI":"10.3217\/JUCS-012-11-1618"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ Report, AMAST Series in Computing, vol.\u00a06. World Scientific (1998)","DOI":"10.1142\/3831"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100497"},{"key":"3_CR7","unstructured":"Fraser, K.: Practical lock-freedom. Ph.D. thesis, University of Cambridge, UK (2004). https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.599193"},{"key":"3_CR8","doi-asserted-by":"publisher","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\u2014Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06269, pp. 388\u2013402. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_27","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Gotsman, A., Rinetzky, N., Yang, H.: Verifying concurrent memory reclamation algorithms with grace. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems\u201422nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07792, pp. 249\u2013269. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_15","DOI":"10.1007\/978-3-642-37036-6_15"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Jung, J., Lee, J., Choi, J., Kim, J., Park, S., Kang, J.: Modular verification of safe memory reclamation in concurrent separation logic. Proc. ACM Program. Lang. 7(OOPSLA2), 828\u2013856 (2023). https:\/\/doi.org\/10.1145\/3622827","DOI":"10.1145\/3622827"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018). https:\/\/doi.org\/10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"3_CR13","unstructured":"Mckenney, P.E., Walpole, J.: Exploiting deferred destruction: an analysis of read-copy-update techniques in operating system kernels. Ph.D. thesis (2004)"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Michael, M.M.: Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distributed Syst. 15(6), 491\u2013504 (2004). https:\/\/doi.org\/10.1109\/TPDS.2004.8","DOI":"10.1109\/TPDS.2004.8"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Nikolaev, R., Ravindran, B.: Universal wait-free memory reclamation. CoRR abs\/2001.01999 (2020). http:\/\/arxiv.org\/abs\/2001.01999","DOI":"10.1145\/3332466.3374540"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Nikolaev, R., Ravindran, B.: Brief announcement: Crystalline: Fast and memory efficient wait-free reclamation. In: Gilbert, S. (ed.) 35th International Symposium on Distributed Computing, DISC 2021, October 4-8, 2021, Freiburg, Germany (Virtual Conference). LIPIcs, vol.\u00a0209, pp. 60:1\u201360:4. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.DISC.2021.60, https:\/\/doi.org\/10.4230\/LIPIcs.DISC.2021.60","DOI":"10.4230\/LIPICS.DISC.2021.60"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Ogata, K., Futatsugi, K.: Proof scores in the OTS\/CafeOBJ method. In: FMOODS 2003, France. vol.\u00a02884, pp. 170\u2013184. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-39958-2_12"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Parkinson, M.J., Bornat, R., O\u2019Hearn, P.W.: Modular verification of a non-blocking stack. In: Hofmann, M., Felleisen, M. (eds.) Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007. pp. 297\u2013302. ACM (2007). https:\/\/doi.org\/10.1145\/1190216.1190261","DOI":"10.1145\/1190216.1190261"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Riesco, A., Ogata, K.: Cimpg+f: A proof generator and fixer-upper for cafeobj specifications. In: Theoretical Aspects of Computing - ICTAC 2020\u201417th International Colloquium, Macau, China, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12545, pp. 64\u201382. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-64276-1_4","DOI":"10.1007\/978-3-030-64276-1_4"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Riesco, A., Ogata, K., Futatsugi, K.: A Maude environment for CafeOBJ. Formal Aspects Comput. 29(2), 309\u2013334 (2017). https:\/\/doi.org\/10.1007\/S00165-016-0398-7","DOI":"10.1007\/S00165-016-0398-7"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: Formal verification of a lock-free stack with hazard pointers. In: Cerone, A., Pihlajasaari, P. (eds.) Theoretical Aspects of Computing - ICTAC 2011\u20148th International Colloquium, Johannesburg, South Africa, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06916, pp. 239\u2013255. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-23283-1_16","DOI":"10.1007\/978-3-642-23283-1_16"},{"key":"3_CR22","unstructured":"Tran, D.D.: Formal verification with algebraic techniques and its application. Ph.D. thesis, Ishikawa 923-1211, Japan (2023). http:\/\/hdl.handle.net\/10119\/18777"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Tran, D.D., Ogata, K.: Formal verification of TLS 1.2 by automatically generating proof scores. Comput. Secur. 123, 102909 (2022). https:\/\/doi.org\/10.1016\/j.cose.2022.102909","DOI":"10.1016\/j.cose.2022.102909"},{"key":"3_CR24","unstructured":"Treiber, R.K.: Systems Programming: Coping with Parallelism. International Business Machines Incorporated, Thomas J. Watson Research Center (2986)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65941-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:11:17Z","timestamp":1722496277000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65941-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031659409","9783031659416"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65941-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WRLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Rewriting Logic and its Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wrla2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/wrla2024.gitlab.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}