IARCS Verification Seminar Series -- Talk by KC Sivaramakrishnan on Nov. 18 at 1900 hrs IST
Dear all, The next talk in the IARCS Verification Seminar Series will be given by KC Sivaramakrishnan, an Assistant Professor in the Computer Science and Engineering department at Indian Institute of Technology, Madras and the Chief Technology Officer of Tarides. The talk is scheduled on Tuesday, November 18, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NjNrcmQ1c2J2bTZ2czk2bHZhY2Q4bmwydHAgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/), and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Organizers, IARCS Verification Seminar Series ============================================================= Title: A Mechanically Verified Garbage Collector for OCaml Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: OCaml is a garbage-collected (GC) language, where unused memory is automatically and reliably freed. OCaml's GC is known for its high throughput and low latency, making it suitable for both batch jobs and interactive systems. OCaml GC is non-trivial and written in C, and is a part of the trusted computing base of OCaml programs. Bugs in the GC have the potential to violate the type safety of OCaml programs. In this talk, I will describe our work in developing a correct, proof-oriented GC for OCaml from scratch, capable of being swapped into the existing OCaml runtime system. Our GC is simple — a stop-the-world mark-and-sweep collector — but is capable of running non-trivial OCaml programs. The GC is developed in F* and its low-level subset Low*, which is compiled to memory-safe C. I will also describe the extension of our collector to enable generational and incremental collection. This work was published in the Journal of Automated Reasoning (link <https://link.springer.com/article/10.1007/s10817-025-09721-0>). Bio: KC Sivaramakrishnan is an Assistant Professor in the Computer Science and Engineering department at Indian Institute of Technology, Madras and the Chief Technology Officer of Tarides. He led the development of Multicore OCaml, a concurrent and parallel extension of the OCaml programming language. His research interest lies in building robust, secure and scalable systems using programming language technology.
Thanks for coming to my talk today. Apologies for going over. Reg one of the questions in the talk about graph isomorphism, Sheera tells me that `successors` returns a sequence (functional list) of successors in the order in which they appear in the object. So `successors g_init x == successors g_sweep x` ensures that pointers are not reordered in an object between the initial and the final heaps. Kind Regards KC On Tue, Nov 18, 2025 at 1:43 AM VSS IARCS <vss.iarcs@gmail.com> wrote:
Dear all,
The next talk in the IARCS Verification Seminar Series will be given by KC Sivaramakrishnan, an Assistant Professor in the Computer Science and Engineering department at Indian Institute of Technology, Madras and the Chief Technology Officer of Tarides. The talk is scheduled on Tuesday, November 18, at 1900 hrs IST (add to Google calendar < https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NjNrcmQ1c2J...
).
The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/), and also appended to the body of this email.
The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas.
All are welcome to join.
Best regards, Organizers, IARCS Verification Seminar Series
=============================================================
Title: A Mechanically Verified Garbage Collector for OCaml
Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194)
Abstract: OCaml is a garbage-collected (GC) language, where unused memory is automatically and reliably freed. OCaml's GC is known for its high throughput and low latency, making it suitable for both batch jobs and interactive systems. OCaml GC is non-trivial and written in C, and is a part of the trusted computing base of OCaml programs. Bugs in the GC have the potential to violate the type safety of OCaml programs. In this talk, I will describe our work in developing a correct, proof-oriented GC for OCaml from scratch, capable of being swapped into the existing OCaml runtime system. Our GC is simple — a stop-the-world mark-and-sweep collector — but is capable of running non-trivial OCaml programs. The GC is developed in F* and its low-level subset Low*, which is compiled to memory-safe C. I will also describe the extension of our collector to enable generational and incremental collection.
This work was published in the Journal of Automated Reasoning (link <https://link.springer.com/article/10.1007/s10817-025-09721-0>).
Bio: KC Sivaramakrishnan is an Assistant Professor in the Computer Science and Engineering department at Indian Institute of Technology, Madras and the Chief Technology Officer of Tarides. He led the development of Multicore OCaml, a concurrent and parallel extension of the OCaml programming language. His research interest lies in building robust, secure and scalable systems using programming language technology. _______________________________________________ FMIndia mailing list -- fmindia@cmi.ac.in To unsubscribe send an email to fmindia-leave@cmi.ac.in
https://fmindia.cmi.ac.in/ _______________________________________________
-- Kind Regards KC Sivaramakrishnan
participants (2)
-
KC Sivaramakrishnan -
VSS IARCS