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.

• 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.

• 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.

• 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