{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T00:10:08Z","timestamp":1750810208638,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_31","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"496-513","source":"Crossref","is-referenced-by-count":5,"title":["Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology"],"prefix":"10.1007","author":[{"given":"Yannick","family":"Zakowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Cachera","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delphine","family":"Demange","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gustavo","family":"Petri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Vitek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Demange, D., Laporte, V., Zhao, L., Jagannathan, S., Pichardie, D., Vitek, J., Plan, B.: a buffered memory model for java. In: POPL 2013, pp. 329\u2013342 (2013)","key":"31_CR1","DOI":"10.1145\/2480359.2429110"},{"issue":"11","key":"31_CR2","doi-asserted-by":"publisher","first-page":"966","DOI":"10.1145\/359642.359655","volume":"21","author":"EW Dijkstra","year":"1978","unstructured":"Dijkstra, E.W., Lamport, L., Martin, A.J., Scholten, C.S., Steffens, E.F.M.: On-the-fly garbage collection: an exercise in cooperation. Commun. ACM 21(11), 966\u2013975 (1978)","journal-title":"Commun. ACM"},{"doi-asserted-by":"crossref","unstructured":"Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: Proceedings POPL 1994, pp. 70\u201383 (1994)","key":"31_CR3","DOI":"10.1145\/174675.174673"},{"doi-asserted-by":"crossref","unstructured":"Doligez, D., Leroy, X.: A concurrent, generational garbage collector for a multithreaded implementation of ML. In: Proceedings of POPL 1993, pp. 113\u2013123 (1993)","key":"31_CR4","DOI":"10.1145\/158511.158611"},{"doi-asserted-by":"crossref","unstructured":"Domani, T., Kolodner, E.K., Lewis, E., Salant, E.E., Barabash, K., Lahan, I., Levanoni, Y., Petrank, E., Yanover, I.: Implementing an on-the-fly garbage collector for Java. In: Proceedings of ISMM 2000, pp. 155\u2013166 (2000)","key":"31_CR5","DOI":"10.1145\/362426.362484"},{"doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Proceedings of POPL 2009, pp. 2\u201315 (2009)","key":"31_CR6","DOI":"10.1145\/1594834.1480885"},{"doi-asserted-by":"crossref","unstructured":"Zakowski, Y., et al.: Verifying a concurrent garbage collector using an RG methodology (2017). http:\/\/www.irisa.fr\/celtique\/ext\/cgc\/","key":"31_CR7","DOI":"10.1007\/978-3-319-66107-0_31"},{"doi-asserted-by":"crossref","unstructured":"Gammie, P., Hosking, A.L., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In: Proceedings of PLDI 2015, pp. 99\u2013109 (2015)","key":"31_CR8","DOI":"10.1145\/2813885.2738006"},{"key":"31_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/3-540-61474-5_103","volume-title":"Computer Aided Verification","author":"G Gonthier","year":"1996","unstructured":"Gonthier, G.: Verifying the safety of a practical concurrent garbage collector. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 462\u2013465. Springer, Heidelberg (1996). doi:10.1007\/3-540-61474-5_103"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1258","DOI":"10.1007\/BFb0098007","volume-title":"Parallel and Distributed Processing","author":"K Havelund","year":"1999","unstructured":"Havelund, K.: Mechanical verification of a garbage collector. In: Rolim, J., et al. (eds.) IPPS 1999. LNCS, vol. 1586, pp. 1258\u20131283. Springer, Heidelberg (1999). doi:10.1007\/BFb0098007"},{"doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Petrank, E.: Automated verification of practical garbage collectors. In: Proceedings of POPL 2009, pp. 441\u2013453 (2009)","key":"31_CR11","DOI":"10.1145\/1594834.1480935"},{"key":"31_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-319-21668-3_26","volume-title":"Computer Aided Verification","author":"C Hawblitzel","year":"2015","unstructured":"Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 449\u2013465. Springer, Cham (2015). doi:10.1007\/978-3-319-21668-3_26"},{"issue":"3","key":"31_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 Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"31_CR14","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/2601339","volume":"36","author":"S Jagannathan","year":"2014","unstructured":"Jagannathan, S., Laporte, V., Petri, G., Pichardie, D., Vitek, J.: Atomicity refinement for verified compilation. ACM Trans. Program. Lang. Syst. 36(2), 6:1\u20136:30 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"31_CR15","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"31_CR16","doi-asserted-by":"publisher","DOI":"10.1201\/9781315388021","volume-title":"Handbook, The Garbage Collection: The Art of Automatic Memory Management","author":"R Jones","year":"2011","unstructured":"Jones, R., Hosking, A., Moss, E.: Handbook, The Garbage Collection: The Art of Automatic Memory Management, 1st edn. Chapman & Hall\/CRC, Boca Raton (2011)","edition":"1"},{"key":"31_CR17","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/2576235","volume":"36","author":"H Liang","year":"2014","unstructured":"Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. Program. Lang. Syst. 36, 3 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"McCreight, A., Chevalier, T., Tolmach, A.P.: A certified framework for compiling and executing garbage-collected languages. In: Proceedings of ICFP 2010, pp. 273\u2013284 (2010)","key":"31_CR18","DOI":"10.1145\/1932681.1863584"},{"doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Reusable Verification of a Copying Collector. In: VSTTE 2010 (2010)","key":"31_CR19","DOI":"10.1007\/978-3-642-15057-9_10"},{"doi-asserted-by":"crossref","unstructured":"Pizlo, F., Ziarek, L., Maj, P., Hosking, A.L., Blanton, E., Vitek, J.: Schism: fragmentation-tolerant real-time garbage collection. In: Proceedings of PLDI (2010)","key":"31_CR20","DOI":"10.1145\/1806596.1806615"},{"key":"31_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-36575-3_24","volume-title":"Programming Languages and Systems","author":"LP Nieto","year":"2003","unstructured":"Nieto, L.P.: The rely-guarantee method in Isabelle\/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 348\u2013362. Springer, Heidelberg (2003). doi:10.1007\/3-540-36575-3_24"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS 2002, pp. 55\u201374 (2002)","key":"31_CR22","DOI":"10.1109\/LICS.2002.1029817"},{"doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Proceedings of PLDI 2015, pp. 77\u201387. ACM (2015)","key":"31_CR23","DOI":"10.1145\/2813885.2737964"},{"key":"31_CR24","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/j.entcs.2011.09.029","volume":"276","author":"V Vafeiadis","year":"2011","unstructured":"Vafeiadis, V.: Concurrent separation logic and operational semantics. Electron. Notes Theor. Comput. Sci. 276, 335\u2013351 (2011)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"31_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-74407-8_18"},{"doi-asserted-by":"crossref","unstructured":"Zakowski, Y., Cachera, D., Demange, D., Pichardie, D.: Compilation of linearizable data structures - a mechanised RG logic for semantic refinement. Technical report (2017). https:\/\/hal.archives-ouvertes.fr\/hal-01538128","key":"31_CR26","DOI":"10.1145\/3167132.3167333"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T23:39:00Z","timestamp":1750808340000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}