{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:52:09Z","timestamp":1770292329331,"version":"3.49.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["14-CE28-0004"],"award-info":[{"award-number":["14-CE28-0004"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation","award":["CCF-1544542"],"award-info":[{"award-number":["CCF-1544542"]}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["695412"],"award-info":[{"award-number":["695412"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1318227"],"award-info":[{"award-number":["CCF-1318227"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1618732"],"award-info":[{"award-number":["CCF-1618732"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["503353"],"award-info":[{"award-number":["503353"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s10817-018-9489-x","type":"journal-article","created":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T10:42:09Z","timestamp":1541068929000},"page":"489-515","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4585-6470","authenticated-orcid":false,"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","published-online":{"date-parts":[[2018,11,1]]},"reference":[{"issue":"1\u20133","key":"9489_CR1","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1\u20133), 227\u2013270 (2007)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"9489_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s10817-015-9324-6","volume":"55","author":"J Davis","year":"2015","unstructured":"Davis, J., Myreen, M.O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it). J. Autom. Reason. 55(2), 117\u2013183 (2015)","journal-title":"J. Autom. Reason."},{"key":"9489_CR3","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software (TACAS) (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9489_CR4","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: Symposium on Principles of Programming Languages (POPL) (2013)","DOI":"10.1145\/2429069.2429110"},{"issue":"11","key":"9489_CR5","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"},{"key":"9489_CR6","doi-asserted-by":"crossref","unstructured":"Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: Symposium on Principles of Programming Languages (POPL) (1994)","DOI":"10.1145\/174675.174673"},{"key":"9489_CR7","doi-asserted-by":"crossref","unstructured":"Doligez, D., Leroy, X.: A concurrent, generational garbage collector for a multithreaded implementation of ML. In: Symposium on Principles of Programming Languages (POPL) (1993)","DOI":"10.1145\/158511.158611"},{"key":"9489_CR8","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: International Symposium on Memory Management (ISMM) (2000)","DOI":"10.1145\/362422.362484"},{"key":"9489_CR9","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Symposium on Principles of Programming Languages (POPL) (2009)","DOI":"10.1145\/1480881.1480885"},{"key":"9489_CR10","doi-asserted-by":"crossref","unstructured":"Gammie, P., Hosking, A.L., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In: Programming Language Design and Implementation (PLDI) (2015)","DOI":"10.1145\/2737924.2738006"},{"key":"9489_CR11","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: Verifying the safety of a practical concurrent garbage collector. In: International Conference on Computer Aided Verification (CAV) (1996)","DOI":"10.1007\/3-540-61474-5_103"},{"key":"9489_CR12","unstructured":"Havelund, K.: Mechanical verification of a garbage collector. In: International Parallel Processing Symposium and Symposium on Parallel and Distributed Processing (IPPS\/SPDP) (1999)"},{"key":"9489_CR13","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: Conference on Operating Systems Design and Implementation (OSDI) (2014)"},{"key":"9489_CR14","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Petrank, E.: Automated verification of practical garbage collectors. In: Symposium on Principles of Programming Languages (POPL) (2009)","DOI":"10.1145\/1480881.1480935"},{"key":"9489_CR15","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: International Conference on Computer Aided Verification (CAV) (2015)","DOI":"10.1007\/978-3-319-21668-3_26"},{"issue":"3","key":"9489_CR16","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. Trans. Program. Lang. Syst. (TOPLAS) 12(3), 463\u2013492 (1990)","journal-title":"Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"2","key":"9489_CR17","first-page":"6","volume":"36","author":"S Jagannathan","year":"2014","unstructured":"Jagannathan, S., Laporte, V., Petri, G., Pichardie, D., Vitek, J.: Atomicity refinement for verified compilation. Trans. Program. Lang. Syst. (TOPLAS) 36(2), 6 (2014)","journal-title":"Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"4","key":"9489_CR18","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. Trans. Program. Lang. Syst. (TOPLAS) 5(4), 596\u2013619 (1983)","journal-title":"Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"9489_CR19","doi-asserted-by":"publisher","DOI":"10.1201\/9781315388021","volume-title":"The Garbage Collection Handbook","author":"R Jones","year":"2011","unstructured":"Jones, R., Hosking, A., Moss, E.: The Garbage Collection Handbook. Chapman & Hall, London (2011)"},{"key":"9489_CR20","unstructured":"Leino, R.: This is boogie 2 (2008). \n                    https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"9489_CR21","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X., Fu, M.: A rely-guarantee-based simulation for verifying concurrent program transformations. In: Symposium on Principles of Programming Languages (POPL) (2012)","DOI":"10.1145\/2103656.2103711"},{"issue":"1","key":"9489_CR22","first-page":"3","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. Trans. Program. Lang. Syst. (TOPLAS) 36(1), 3 (2014)","journal-title":"Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"9489_CR23","doi-asserted-by":"crossref","unstructured":"McCreight, A., Chevalier, T., Tolmach, A.: A certified framework for compiling and executing garbage-collected languages. In: International Conference on Functional Programming (ICFP) (2010)","DOI":"10.1145\/1863543.1863584"},{"key":"9489_CR24","doi-asserted-by":"crossref","unstructured":"McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: Programming Language Design and Implementation (PLDI) (2007)","DOI":"10.1145\/1250734.1250788"},{"key":"9489_CR25","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Symposium on Principles of Distributed Computing (PODC) (1996)","DOI":"10.21236\/ADA309412"},{"key":"9489_CR26","doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Reusable verification of a copying collector. In: Conference on Verified Software: Theories, Tools, Experiments (VSTTE) (2010)","DOI":"10.1007\/978-3-642-15057-9_10"},{"key":"9489_CR27","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Separation logic and concurrent resource management. In: International Symposium on Memory Management (ISMM) (2007)","DOI":"10.1145\/1296907.1296908"},{"issue":"4","key":"9489_CR28","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inform. 6(4), 319\u2013340 (1976)","journal-title":"Acta Inform."},{"key":"9489_CR29","doi-asserted-by":"crossref","unstructured":"Pavlovic, D., Pepper, P., Smith, D.R.: Formal derivation of concurrent garbage collectors. In: International Conference on Mathematics of Program Construction (MPC) (2010)","DOI":"10.1007\/978-3-642-13321-3_20"},{"key":"9489_CR30","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Programming Language Design and Implementation (PLDI) (1988)","DOI":"10.1145\/53990.54010"},{"key":"9489_CR31","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: Programming Language Design and Implementation (PLDI) (2010)","DOI":"10.1145\/1806596.1806615"},{"key":"9489_CR32","doi-asserted-by":"crossref","unstructured":"Prensa Nieto, L.: the rely-guarantee method in Isabelle\/HOL. In: European Conference on Programming (ESOP) (2003)","DOI":"10.1007\/3-540-36575-3_24"},{"key":"9489_CR33","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Symposium on Logic in Computer Science (LICS) (2002)"},{"key":"9489_CR34","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/978-3-319-66107-0_28","volume-title":"Interactive Theorem Proving","author":"A Sandberg Ericsson","year":"2017","unstructured":"Sandberg Ericsson, A., Myreen, M.O., \u00c5man Pohjola, J.: A verified generational garbage collector for CakeML. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C. (eds.) Interactive Theorem Proving, pp. 444\u2013461. Springer, Cham (2017)"},{"key":"9489_CR35","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Programming Language Design and Implementation (PLDI) (2015)","DOI":"10.1145\/2737924.2737964"},{"issue":"3","key":"9489_CR36","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J \u0160ev\u010d\u00edk","year":"2013","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Nardelli, F.Z., Jagannathan, S., Sewell, P.: CompcertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22 (2013)","journal-title":"J. ACM"},{"issue":"4","key":"9489_CR37","first-page":"24","volume":"30","author":"N Torp-Smith","year":"2008","unstructured":"Torp-Smith, N., Birkedal, L., Reynolds, J.C.: Local reasoning about a copying garbage collector. Trans. Program. Lang. Syst. (TOPLAS) 30(4), 24 (2008)","journal-title":"Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"9489_CR38","unstructured":"Treiber, R.K.: Systems programming: coping with parallelism. Technical report, IBM Almaden Research Center (1986)"},{"key":"9489_CR39","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":"9489_CR40","unstructured":"Vafeiadis, V., Parkinson, M.J.: A marriage of rely\/guarantee and separation logic. In: International Conference on Concurrency Theory (CONCUR) (2007)"},{"key":"9489_CR41","doi-asserted-by":"crossref","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Programming Language Design and Implementation (PLDI) (2010)","DOI":"10.1145\/1806596.1806610"},{"key":"9489_CR42","unstructured":"Zakowski, Y., Cachera, D., Demange, D., Petri, G., Pichardie, D., Jagannathan, S., Vitek, J.: Verifying a concurrent garbage collector using a rely-guarantee methodology\u2014companion website (2017). \n                    http:\/\/www.irisa.fr\/celtique\/ext\/cgc\/\n                    \n                  . Accessed 31 Oct 2018"},{"key":"9489_CR43","doi-asserted-by":"crossref","unstructured":"Zakowski, Y., Cachera, D., Demange, D., Pichardie, D.: Compilation of linearizable data structures\u2014a mechanised RG logic for semantic refinement. In: Symposium on Applied Computing (SAC) (2018)","DOI":"10.1145\/3167132.3167333"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9489-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9489-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9489-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T23:02:44Z","timestamp":1589410964000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9489-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,1]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["9489"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9489-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11,1]]},"assertion":[{"value":"27 February 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 October 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 November 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}