Hello there! I am Ramneet, 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 that scale to 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. In my thesis, I 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.
Download my resumé.
- Formal Methods (esp. Program Logics)
- Theorem Proving
- Program Synthesis
- Artificial Intelligence
M. Tech. in Computer Science & Engineering, 2023-2024, CGPA: 9.398
Indian Institute of Technology Delhi, India
B. Tech. in Computer Science & Engineering, 2019-2023, CGPA: 9.372
Indian Institute of Technology Delhi, India
Recent News
[22/07/2025] : My Master thesis work at Georgia Tech with Suguman Bansal was accepted to the International Conference on Computer-Aided Verification (CAV) 2025. See the paper here and the thesis here.
[09/06/2025] : We released Code Researcher - a deep research agent that can fix crashes in large systems codebases (e.g., the Linux kernel) by gathering context from the codebase and commit history.
[01/01/2024] : Excited to be a Teaching Assistant for two courses (!!) at IIT Delhi this semester – COL726 : Numerical Analysis and Scientific Computing and COL728 : Compiler Design. I learned a ton from both these courses when I took them, and I hope to learn another ton this time.
Experience
(looking for more)
AI Agents and Models for Large-Scale Enterprise-Grade Software Engineering
- Designed Code Researcher, a deep research agent for resolving crashes in large systems codebases (like the Linux kernel) by gathering context from the codebase and the commit history.
- On the Linux kernel crash benchmark kBenchSyz (200 bugs), Code Researcher achieves a 58% crash-resolution rate, significantly outperforming SWE-agent’s 37.5%.
Probabilistic Model Checking (CAV 2025 Paper, Master Thesis)
- Designed a novel symbolic (i.e., using BDDs) algorithm for the Maximal End Component (MEC) Decomposition of Markov Decision Processes (MDP), a fundamental problem in probabilistic model checking.
- Implemented the algorithm in a custom fork of the Storm probabilistic model checker.
- Solved 19 more benchmarks (168/368 with 4 mins timeout) than the closest previous algorithm, and achieved 2.24x speedup on the ones that both solved, making this the empirically fastest currently.
Infrastructure Team
- Built tooling for secure key management and encryption of servers.
- Maintained,scaled & monitored existing infrastructure, including bare metal servers,cloudmachines, & a Kubernetes cluster, to allow the organization to provide secure & reliable industry‐leading Proof‐of‐Stake validation services.
Marketing Segment Flow Prediction
- Developed a novel temporal‐graph‐based model for marketing segments.
- Applied neural embedding techniques for temporal graphs to predict node features and edge weights, used for forecasting churn and flow of customers between segments.
- Designed network centrality & flow‐based measures to identify high‐activity segments, providing insights about market behaviour to marketers.
Data Driven Marketing Spend Optimization
- Developed a system to give optimal spend recommendations across media channels & adsets using historical marketing data, allowing marketing teams to focus on creativity and design.
- Implemented a revenue forecasting model to predict the revenue-budget relationship for each channel and adset, taking into account adstock transformation as well as the diminshing nature of returns. Dealt effectively with sparsity of data at the adset level.
- Implemented a cross-channel optimiser which used revenue forecasting models at both hierarchical levels to provide optimal spend allocations. Incorporated constraints like minimum/maximum channel spend keeping in mind practical marketing strategies.
Featured Publications
Projects
Accomplishments
Get In Touch!
Feel free to contact me :)