Who am I?

Hi, I'm Kiran (കിരൺ) Gopinathan! I'm a fifth-year PhD candidate at the School of Computing at NUS advised by Ilya Sergey in VERSE Lab.

My research focuses on 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. Notable highlights of my work include: producing the first formally verified proof of the probabilistic properties of the Bloom Filter data structure; 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.

As a hacker, I develop several pieces of Free and Libre software that not only respects their users' freedoms but also makes their lives better (see also my GitHub profile), and maintain a popular web-blog where I write up fun and interesting results from my research in a more accessible and inclusive format for the general public.

I completed my undergraduate degree in Computer Science at University College London. In the past, I've worked in a range of CS disciplines, from the design of interoperable data formats to industrial machine learning for insurance companies, though my main focus now lies within the use of formal methods for reasoning about algorithms.

Curriculum Vitae

The latest copy of my CV can be found here.

Contact Me

Feel free to send me an email at "kirang@comp.nus.edu.sg".

Publications

Conference Papers

  • 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 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
    • Authors: 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

Notable Projects & Software

  • Sisyphus: Tool for automated repair of proofs of OCaml programs [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]

Click here to see all my projects.

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 our 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

  • 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
  • CS5232: Formal Specification and Design Techniques, 2023 - Guest Lecturer
  • 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