Grounded Deduction
Summer Research Fellow | EPFL, Switzerland (Onsite) | May 2026 – Present
Adviser: Prof. Bryan Ford, DEDIS Lab
- Formally reasoning about and developing the novel logical framework "Grounded Deduction" in the Isabelle proof assistant.
Game Theory and Automata
Student Researcher | IISc | Jan 2026 – Present
- Investigating supergames played by finite automatons under finite costs for complexity to analyze the sequential collapse of equilibrium states.
- Deriving critical phase change thresholds that characterize these equilibrium dynamics.
Causal Discovery in Time Series
Student Researcher | IISc | Aug 2025 – May 2026
Adviser: Prof. Deepak N. Subramani, Computational and Data Sciences, IISc
- Designed a novel Transformer architecture for causal discovery in time series data.
- Developed a trainable attention mask mechanism based on forecasting objectives to learn the underlying causal graph structure, inspired by principles of causal inference.
Under Review at NeurIPS
[Paper]
|
[Code]
Verification Modulo Tested Library Contracts
Student Researcher | IISc | May 2025 – Apr 2026
Advisers: Prof. D. D'Souza (IISc), Prof. M. Parthasarathy (UIUC), Prof. A. Murali (UW-Madison)
- Co-developed VMTLC, a hybrid framework that verifies client programs by synthesizing library specifications that are formally proven against the client but validated via testing against the library.
- Designed the Learner component within a Teacher-Learner CEGIS loop, developing two distinct LLM-integrated architectures (a pure LLM learner and an LLM-seeded ICE learner) to leverage semantic intuition, synthesizing valid contracts where traditional enumerative baselines could not.
- Designed and built the core LLM pipeline responsible for generating contracts from logical rules and integrated it into a feedback loop with formal verifiers and testing engines to ensure correctness.
Accepted to PLDI 2026
[Paper]
|
[Code]
Enhancing Formal Verification with LLMs
Research Intern | University of Virginia, USA (Remote) | Aug 2025 – Oct 2025
Adviser: Prof. Wenxi Wang, The University of Virginia
- Developed ACPRO, a framework that uses a multi-agent LLM pipeline to transform low-level Z3 proofs into interpretable, high-level Verus verification steps.
- This work also produced the VSVerus dataset, a new resource for studying fine-grained LLM reasoning in formal verification.
Formalization of Group Theoretic Algorithms
Summer Research Fellow | Krea University, India (Onsite) | May 2025 – July 2025
Advisers: Prof. Rishi Vyas (KREA), Prof. T.V.H Prathamesh (KREA)
- Formalized proofs for decision problems in geometric group theory (including the word, conjugacy, and subgroup membership problems) using the Lean 4 proof assistant.
- Key contributions include formalizing two definitions of the Dehn function and proving their equivalence and verifying the algorithm for the conjugacy problem in free groups.
- Current work focuses on the computability of the Dehn function for hyperbolic groups.
