{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T13:57:09Z","timestamp":1787061429411,"version":"build-2736575974"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T00:00:00Z","timestamp":1747180800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T00:00:00Z","timestamp":1747180800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>The OCaml programming language finds application across diverse domains, including systems programming, web development, scientific computing, formal verification, and symbolic mathematics. OCaml is a memory-safe programming language that uses a garbage collector (GC) to free unreachable memory. It features a low-latency, high-performance GC, tuned for functional programming. The GC has two generations\u2014a minor heap collected using a copying collector and a major heap collected using an incremental mark-and-sweep collector. Alongside the intricacies of an efficient GC design, OCaml compiler uses efficient object representations for some object classes, such as interior pointers for supporting mutually recursive functions, which further complicates the GC design. The GC is a critical component of the OCaml runtime system, and its correctness is essential for the safety of OCaml programs. In this paper, we propose a strategy for crafting a correct, proof-oriented GC from scratch, designed to evolve over time with additional language features. Our approach neatly separates abstract GC correctness from OCaml-specific GC correctness, offering the ability to integrate further GC optimizations, while preserving core abstract GC correctness. As an initial step to demonstrate the viability of our approach, we have developed a verified stop-the-world mark-and-sweep GC for OCaml. The approach is fully mechanized in F* and its low-level subset Low*. We use the KaRaMel compiler to compile Low* to C, and integrate the verified GC with the OCaml runtime. Our GC is evaluated against off-the-shelf OCaml GC and Boehm\u2013Demers\u2013Weiser conservative GC, and the experimental results show that verified OCaml GC is competitive with the standard OCaml GC.<\/jats:p>","DOI":"10.1007\/s10817-025-09721-0","type":"journal-article","created":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T11:16:47Z","timestamp":1747221407000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Mechanically Verified Garbage Collector for OCaml"],"prefix":"10.1007","volume":"69","author":[{"given":"Sheera","family":"Shamsu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dipesh","family":"Kafle","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dhruv","family":"Maroo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kartik","family":"Nagar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karthikeyan","family":"Bhargavan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"KC","family":"Sivaramakrishnan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,14]]},"reference":[{"key":"9721_CR1","unstructured":"Bhargavan, K., Bond, B., Delignat-Lavaud, A., Fournet, C., Hawblitzel, C., Hritcu, C., Ishtiaq, S., Kohlweiss, M., Leino, R., Lorch, J., et al.: Everest: towards a verified, drop-in replacement of https. In: 2nd Summit on Advances in Programming Languages (SNAPL 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)"},{"issue":"9","key":"9721_CR2","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1002\/spe.4380180902","volume":"18","author":"H-J Boehm","year":"1988","unstructured":"Boehm, H.-J., Weiser, M.: Garbage collection in an uncooperative environment. Softw. Pract. Exp. 18(9), 807\u2013820 (1988)","journal-title":"Softw. Pract. Exp."},{"key":"9721_CR3","unstructured":"Burdy, L.: B vs. Coq to prove a garbage collector. In: the 14th International Conference on Theorem Proving in Higher Order Logics: Supplemental Proceedings (2001)"},{"key":"9721_CR4","unstructured":"Chen, R., Cohen, C., L\u00e9vy, J.-J., Merz, S., Th\u00e9ry, L.: Formal proofs of tarjan\u2019s strongly connected components algorithm in why3, coq and isabelle. In: ITP 2019\u201410th International Conference on Interactive Theorem Proving, vol. 141, pp. 13-1. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)"},{"issue":"6","key":"9721_CR5","doi-asserted-by":"publisher","first-page":"815","DOI":"10.1093\/logcom\/13.6.815","volume":"13","author":"S Coupet-Grimal","year":"2003","unstructured":"Coupet-Grimal, S., Nouvet, C.: Formal verification of an incremental garbage collector. J. Logic Comput. 13(6), 815\u2013833 (2003)","journal-title":"J. Logic Comput."},{"issue":"2","key":"9721_CR6","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s10817-018-9487-z","volume":"63","author":"AS Ericsson","year":"2019","unstructured":"Ericsson, A.S., Myreen, M.O., Pohjola, J.\u00c5.: A verified generational garbage collector for CakeML. J. Autom. Reason. 63(2), 463\u2013488 (2019)","journal-title":"J. Autom. Reason."},{"key":"9721_CR7","unstructured":"F* team: Pulse: Proof-oriented Programming in Concurrent Separation Logic. https:\/\/fstar-lang.org\/tutorial\/book\/pulse\/pulse.html Accessed 04 Dec 2024"},{"issue":"6","key":"9721_CR8","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1145\/1133255.1134028","volume":"41","author":"X Feng","year":"2006","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. ACM SIGPLAN Not. 41(6), 401\u2013414 (2006)","journal-title":"ACM SIGPLAN Not."},{"key":"9721_CR9","doi-asserted-by":"publisher","unstructured":"Fromherz, A., Rastogi, A., Swamy, N., Gibson, S., Mart\u00ednez, G., Merigoux, D., Ramananandro, T.: Steel: proof-oriented programming in a dependently typed concurrent separation logic. Proc. ACM Program. Lang. 5(ICFP) (2021). https:\/\/doi.org\/10.1145\/3473590","DOI":"10.1145\/3473590"},{"issue":"6","key":"9721_CR10","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1145\/2813885.2738006","volume":"50","author":"P Gammie","year":"2015","unstructured":"Gammie, P., Hosking, A.L., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86 TSO. ACM SIGPLAN Not. 50(6), 99\u2013109 (2015)","journal-title":"ACM SIGPLAN Not."},{"key":"9721_CR11","unstructured":"Goguen, H., Brooksby, R., Burstall, R.: An abstract formulation of memory management. Technical report, University of Edinburgh, December (1998)"},{"key":"9721_CR12","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: Verifying the safety of a practical concurrent garbage collector. In: Computer Aided Verification: 8th International Conference, CAV\u201996 New Brunswick, NJ, USA, 31 July\u20133 August 1996 Proceedings 8, pp. 462\u2013465. Springer, Berlin (1996)","DOI":"10.1007\/3-540-61474-5_103"},{"key":"9721_CR13","unstructured":"Gouy, I.: The Computer Language Benchmarks Game. https:\/\/benchmarksgame-team.pages.debian.net\/benchmarksgame\/"},{"key":"9721_CR14","unstructured":"Gu\u00e9neau, A., Jourdan, J.-H., Chargu\u00e9raud, A., Pottier, F.: Formal proof and analysis of an incremental cycle detection algorithm. In: Interactive Theorem Proving. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)"},{"key":"9721_CR15","unstructured":"Havelund, K.: Mechanical verification of a garbage collector. In: Parallel and Distributed Processing: 11th IPPS\/SPDP\u201999 Workshops Held in Conjunction with the 13th International Parallel Processing Symposium and 10th Symposium on Parallel and Distributed Processing San Juan, Puerto Rico, USA, 12\u201316 April 1999 Proceedings 13, pp. 1258\u20131283. Springer (1999)"},{"issue":"1","key":"9721_CR16","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1145\/1594834.1480935","volume":"44","author":"C Hawblitzel","year":"2009","unstructured":"Hawblitzel, C., Petrank, E.: Automated verification of practical garbage collectors. ACM SIGPLAN Not. 44(1), 441\u2013453 (2009)","journal-title":"ACM SIGPLAN Not."},{"key":"9721_CR17","doi-asserted-by":"crossref","unstructured":"Jackson, P.B.: Verifying a garbage collection algorithm. In: Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs\u2019 98 Canberra, Australia 27 September\u20131 October 1998, Proceedings 11, pp. 225\u2013244. Springer (1998)","DOI":"10.1007\/BFb0055139"},{"key":"9721_CR18","doi-asserted-by":"publisher","DOI":"10.1201\/9781420082807","volume-title":"The Garbage Collection Handbook: The Art of Automatic Memory Management","author":"R Jones","year":"2016","unstructured":"Jones, R., Hosking, A., Moss, E.: The Garbage Collection Handbook: The Art of Automatic Memory Management. CRC Press, Boca Raton (2016)"},{"key":"9721_CR19","doi-asserted-by":"crossref","unstructured":"Lammich, P., Neumann, R.: A framework for verifying depth-first search algorithms. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, pp. 137\u2013146 (2015)","DOI":"10.1145\/2676724.2693165"},{"issue":"1","key":"9721_CR20","first-page":"67","volume":"3","author":"C Lin","year":"2009","unstructured":"Lin, C., Chen, Y., Hua, B.: Verification of an incremental garbage collector in Hoare-style logic. Int. J. Softw. Informatics 3(1), 67\u201388 (2009)","journal-title":"Int. J. Softw. Informatics"},{"issue":"3","key":"9721_CR21","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/s11390-007-9049-z","volume":"22","author":"C-X Lin","year":"2007","unstructured":"Lin, C.-X., Chen, Y.-Y., Li, L., Hua, B.: Garbage collector verification for proof-carrying code. J. Comput. Sci. Technol. 22(3), 426\u2013437 (2007)","journal-title":"J. Comput. Sci. Technol."},{"key":"9721_CR22","doi-asserted-by":"publisher","DOI":"10.1017\/9781009129220","volume-title":"Real World OCaml: Functional Programming for the Masses","author":"A Madhavapeddy","year":"2022","unstructured":"Madhavapeddy, A., Minsky, Y.: Real World OCaml: Functional Programming for the Masses. Cambridge University Press, Cambridge (2022)"},{"key":"9721_CR23","doi-asserted-by":"crossref","unstructured":"Mart\u00ednez, G., Ahman, D., Dumitrescu, V., Giannarakis, N., Hawblitzel, C., Hri\u0163cu, C., Narasimhamurthy, M., Paraskevopoulou, Z., Pit-Claudel, C., Protzenko, J., et al.: Meta-f: Proof automation with SMT, tactics, and metaprograms. In: Programming Languages and Systems: 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, 6\u201311 April 2019, Proceedings, pp. 30\u201359. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"9721_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: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 468\u2013479 (2007)","DOI":"10.1145\/1250734.1250788"},{"key":"9721_CR25","unstructured":"Mccreight, A.E.: The mechanized verification of garbage collector implementations. PhD thesis, Yale University (2008)"},{"key":"9721_CR26","unstructured":"Mo, M.Y.: Chrome in-the-wild bug analysis: CVE-2021-37975 (2021). https:\/\/securitylab.github.com\/research\/in_the_wild_chrome_cve_2021_37975\/"},{"key":"9721_CR27","doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Reusable verification of a copying collector. In: International Conference on Verified Software: Theories, Tools, and Experiments, pp. 142\u2013156. Springer (2010)","DOI":"10.1007\/978-3-642-15057-9_10"},{"key":"9721_CR28","doi-asserted-by":"publisher","unstructured":"Protzenko, J., Zinzindohou\u00e9, J.-K., Rastogi, A., Ramananandro, T., Wang, P., Zanella-B\u00e9guelin, S., Delignat-Lavaud, A., Hritcu, C., Bhargavan, K., Fournet, C., Swamy, N.: Verified Low-Level Programming Embedded in F*. arXiV Preprint (2018). https:\/\/doi.org\/10.48550\/arXiv.1703.00053","DOI":"10.48550\/arXiv.1703.00053"},{"key":"9721_CR29","unstructured":"Ramananandro, T., Delignat-Lavaud, A., Fournet, C., Swamy, N., Chajed, T., Kobeissi, N., Protzenko, J.: $$\\{$$EverParse$$\\}$$: verified secure $$\\{$$Zero-Copy$$\\}$$ parsers for authenticated message formats. In: 28th USENIX Security Symposium (USENIX Security 19), pp. 1465\u20131482 (2019)"},{"key":"9721_CR30","doi-asserted-by":"publisher","DOI":"10.1145\/3689773","author":"A Reitz","year":"2024","unstructured":"Reitz, A., Fromherz, A., Protzenko, J.: Starmalloc: verifying a modern, hardened memory allocator. Proc. ACM Program. Lang. (2024). https:\/\/doi.org\/10.1145\/3689773","journal-title":"Proc. ACM Program. Lang."},{"key":"9721_CR31","unstructured":"Reynolds, J.C.: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society (2002)"},{"issue":"4","key":"9721_CR32","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/BF01211305","volume":"6","author":"DM Russinoff","year":"1994","unstructured":"Russinoff, D.M.: A mechanically verified incremental garbage collector. Formal Asp. Comput. 6(4), 359\u2013390 (1994)","journal-title":"Formal Asp. Comput."},{"key":"9721_CR33","doi-asserted-by":"crossref","unstructured":"Sivaramakrishnan, K., Dolan, S., White, L., Jaffer, S., Kelly, T., Sahoo, A., Parimala, S., Dhiman, A., Madhavapeddy, A.: Retrofitting parallelism onto OCAML. Proc ACM Program. Lang. 4(ICFP), 1\u201330 (2020)","DOI":"10.1145\/3408995"},{"key":"9721_CR34","doi-asserted-by":"crossref","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.-Y., Kohlweiss, M., et al.: Dependent types and multi-monadic effects in f. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 256\u2013270 (2016)","DOI":"10.1145\/2837614.2837655"},{"key":"9721_CR35","doi-asserted-by":"crossref","unstructured":"Wan, Z., Lo, D., Xia, X., Cai, L.: Bug characteristics in blockchain systems: a large-scale empirical study. In: 2017 IEEE\/ACM 14th International Conference on Mining Software Repositories (MSR), pp. 413\u2013424. IEEE (2017)","DOI":"10.1109\/MSR.2017.59"},{"key":"9721_CR36","doi-asserted-by":"publisher","unstructured":"Wang, S., Cao, Q., Mohan, A., Hobor, A.: Certifying graph-manipulating C programs via localizations within data structures. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360597","DOI":"10.1145\/3360597"},{"key":"9721_CR37","doi-asserted-by":"crossref","unstructured":"Xu, B., Moss, E., Blackburn, S.M.: Towards a model checking framework for a new collector framework. In: Proceedings of the 19th International Conference on Managed Programming Languages and Runtimes, pp. 128\u2013139 (2022)","DOI":"10.1145\/3546918.3546923"},{"issue":"3","key":"9721_CR38","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0164-1212(90)90084-Y","volume":"11","author":"T Yuasa","year":"1990","unstructured":"Yuasa, T.: Real-time garbage collection on general-purpose machines. J. Syst. Softw. 11(3), 181\u2013198 (1990)","journal-title":"J. Syst. Softw."},{"key":"9721_CR39","doi-asserted-by":"crossref","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. In: Interactive Theorem Proving: 8th International Conference, ITP 2017, Bras\u00edlia, Brazil, 26\u201329 September 2017, Proceedings, vol. 8, pp. 496\u2013513. Springer (2017)","DOI":"10.1007\/978-3-319-66107-0_31"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09721-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09721-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09721-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T05:04:13Z","timestamp":1750655053000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09721-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,14]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["9721"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09721-0","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-4674167\/v1","asserted-by":"object"}]},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,14]]},"assertion":[{"value":"2 July 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 February 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"11"}}