IARCS Verification Seminar Series -- Talk by KC Sivaramakrishnan on Nov. 18 at 1900 hrs IST - FMIndia

18 Nov 2025

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.