About

Hi, I’m Ramneet.

Ramneet standing in front of the Golden Gate Bridge wearing a blue t-shirt and a black jacket. — That one photo I'll use on every platform for 10 years.

I am a Research Fellow at Microsoft Research India. My research interests include formal methods (particularly program logics for verification), theorem proving, programming languages and machine learning. I spend time thinking about what are the right abstractions for building reliable software systems on top of fundamentally unreliable ML-models (in particular, LLMs). I believe that “traditional” PL analysis/verification techniques can help in designing LLM-based systems, and taking a formal languages approach can even allow us to understand them more principally/build better ML models.

Aside from how PL can help ML, I also think about how PL problems and, more broadly, the software engineering community (“What will software engineering look like in 10 years?” keeps me up at night) can benefit from the (lightning-speed) advances in machine learning. That forms my work at MSR with Aditya Kanade and Nagarajan Natarajan, where we work on developing AI models and agents for software engineering on large enterprise-grade codebases (e.g., the Linux kernel). I led the Code Researcher project, a deep research agent that can iteratively explore and gather context from large systems codebases and the commit history (a first in the coding agents space). Code Researcher was able to generate crash-resolving patches for a significant number of Linux kernel crashes in our evaluation.

In a prior life, I was a student in the CSE Department at IIT Delhi, where my coursework focussed on formal verification, type theory, semantics of PLs and compilers. For my Master thesis, I was a Research Assistant in the School of Computer Science at Georgia Institute of Techology, working with Prof. Suguman Bansal. My thesis developed INTERLEAVE, a faster symbolic (i.e., using Binary Decision Diagrams) algorithm for computing the Maximal End Components (MECs) of a Markov Decision Process. MEC decomposition is a foundational problem in probabilistic model checking, and our paper was accepted to the International Conference on Computer Aided Verification (CAV) 2025. You can read more about me here and take a look at my personal website to know more about my work experience and projects.