GeezerVison is showing kirancodes.me — Kiran's home page~ - To Proof Maintenance for all and beyond!!!
Kiran Gopinathan
Who am I?
Hi, I'm Kiran (she/her)! I am currently a Research Scientist working
on AI+PL at the Basis Research Institute. Previously I was a
Postdoctoral Researcher at the University of Illinois Urbana
Champaign, advised by Talia Ringer. Before then, I completed my PhD
from the National University of Singapore advised by Ilya Sergey in
VERSE Lab.
My academic research focused on the problem of proof maintenance:
developing newer and better tools for the maintenance and automation
of formal verification—the process of using computers to construct
mathematical proofs about the software correctness—and covers a
broad range of techniques, such as proof repair, invariant inference
or automated verification. See my research statement.
Notable highlights of my work include: producing the first formally
verified proof of the probabilistic properties of the Bloom Filter;
inventing proof-driven testing, a novel technique that exploits
fundamental mathematical truths (the Curry-Howard correspondence) and
enables repairing the proofs of real-world programs.
Other fun facts about me: I am a trans woman (egg cracked 12/2023,
started HRT 20/04/2024); I sometimes make games in my free time (my
itch.io page), I'm a hobbyist artist and use artwork to capture
aspects of my lived experiences, and sometimes I write code.
A selfie of me~
Curriculum Vitae
The latest copy of my CV can be found here.
Publications
Thesis
- Scaling the Evolution of Verified Software - PhD Thesis [pdf]
Kiran Gopinathan
Conference Papers
- Accelerating Automated Program Verifiers by Automatic Proof Localization - CAV 2025 [pdf, code]
Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Müller, Markus Püschel, Ilya Sergey
- Sound and efficient generation of Data-Oriented exploits via programming language synthesis - USENIX 2025 [pdf, code]
Yuxi Ling, Gokul Rajiv, Kiran Gopinathan, Ilya Sergey
- Concurrent Data Structures Made Easy - OOPSLA 2024 [pdf, code, code(rust)]
Callista Le, Kiran Gopinathan, Koon Wen Lee, Ilya Sergey
- Adventure of a Lifetime: Extract Method Refactoring for Rust - OOPSLA 2023 [pdf, code]
Sewen Thy, Andrea Costea, Kiran Gopinathan, Ilya Sergey
- Rhombus: A New Spin on Macros Without All the Parentheses - OOPSLA 2023 [pdf, code]
Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, Sam Tobin-Hochstadt
- Mostly Automated Proof Repair for Verified Libraries - PLDI 2023 [pdf, slides, code]
Kiran Gopinathan, Mayank Keoliya, Ilya Sergey
ACM SIGPLAN Award Awarded ACM SIGPLAN Distinguished Paper Award
- Certifying the Synthesis of Heap-Manipulating Programs - ICFP 2021 [pdf, code]
Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, Ilya Sergey
- Ceramist: Certifying Certainty and Uncertainty in Approximate Membership Query Structures - CAV 2020 [pdf, slides, poster, code]
Kiran Gopinathan, Ilya Sergey
- FHIR-FLI: An Open Source Platform for Sharing Healthcare Data - ICT4AWE 2018
Kiran Gopinathan, Nikolaos Alexandros Kaloumenos, Kinnari Ajmera, Alexandru Matei, Ian Williams, Andrew Davis
Workshop Papers
- Towards Optimising Certified Programs by Proof Rewriting - EGRAPHS 2022 [pdf, slides]
Kiran Gopinathan, Ilya Sergey
- GopCaml: A Structural Editor for OCaml - OCaml Workshop 2021 [pdf, slides, code]
Kiran Gopinathan
- Probchain: Towards Mechanising Probabilistic Properties of a Blockchain - CoqPL 2019 [pdf, slides, code]
Kiran Gopinathan, Ilya Sergey
Awards
- NUS School of Computing Dean's Graduate Research Excellence Award 2023
Given to senior PhD students who have made significant research achievements during their PhD study.
- ACM SIGPLAN Distinguished Paper Award, PLDI 2023
Recieved a distinguished paper award for my work on "Mostly Automated Proof Repair for Verified Libraries".
- Silver Medal for Student Research Competition, PLDI 2020
For poster and presentation on Certifying Bloom Filters.
Service
Mentoring, Volunteering and Event Organisation
Program Committee Member
- OOPSLA 2026
- ICFP 2025
- OCaml Workshop 2023
- AIPLANS 2021
External Reviewer
- ICSE 2024
- OOPSLA 2023
- POPL 2022
- ESOP 2022
- CPP 2021
- CPP 2020
Artefact Evaluation Committee
- PLDI 2021
- ICFP 2021
- PLDI 2020
Teaching
- CS6217: Topics in Programming Languages & Software Engineering, 2023 - Guest Lecturer
Gave seminar on "Program Logics for Functional Languages"
- CS5232: Formal Specification and Design Techniques, 2023 - Guest Lecturer
Gave seminar on Dafny and "Introduction to Floyd-Hoare Logic"
- CS5223: Distributed Systems, 2020-2023 - Teaching Assistant
- CS4215: Programming Languages Implementation, 2020-2022 - Teaching Assistant
- CS5218: Principles and Practice of Program Analysis, 2021 - Teaching Assistant
- CS1010E: Programming Methodology, 2019 - Teaching Assistant
Notable Projects & Software
- Sisyphus: Tool for automated repair of proofs of OCaml programs [code]
- Cleango: Clingo bindings and DSL for Lean4 (10 Stars) [code]
- Ceramist: Verified hash-based Bloom Filters in Coq (120 Stars) [code]
- Gopcaml mode: Emacs plugin Structural editing of OCaml code [code]
- Petrol: Typed SQL DSL for OCaml (85 Stars) [code]
- Ego: Pure OCaml E-graphs library (50 Stars) [code]
- OCamlot: Activitypub server in OCaml (64 Stars) [code]
|