I have completed my M.Tech and Ph.D. in Computer Science and Engineering from IIT Kanpur. My doctoral thesis work is on Program Analysis and Reasoning over Diverse Domains, and my master's thesis work is on Relational Synthesis. My core area of research is Formal Methods, Program Analysis, and Program Verification. I was supervised by Dr. Subhajit Roy who helped me gain a deeper understanding and appreciation of Computer Science.
I am an expert full-stack developer and researcher with expertise in KLEE, LLVM, AFLplusplus, Z3, CVC4, PyTorch, Scikit-learn, Keras, LangGraph, Cline, Agno, FastMCP, and many more. I love to solve real-world problems with robust engineering at scale, blending both theory-rich CS, software engineering, and system design.
- Have a Look at my Development Profile
- I love software architecture and system design.
- https://sumit.reasonlearn.com/
- Our work on LLM-Driven Unsatisfiability Proofs got accepted at 40th ACM Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA2 2026). LLM-Assisted Unsatisfiability Proofs for Satisfiability Modulo Theories, Oracles, and Natural Language
- Our work on Puzzle Generation got accepted at the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024). Program Synthesis Meets Visual What-Comes-Next Puzzles
- Our work on Chiron Framework got accepted at the 38th IEEE/ACM International Conference on Automated Software Engineering (ASE 2023). An Integrated Program Analysis Framework for Graduate Courses in Programming Languages and Software Engineering
- My Doctoral Symposium at SPLASH 2022 (OOPSLA2 2022). https://2022.splashcon.org/details/splash-2022-Doctoral-Symposium/8/Verification-of-Programs-with-Concealed-Components
- Our work on Symbolic Execution for Randomized Programs got accepted in OOPSLA 2022 (Round 2). https://dl.acm.org/doi/10.1145/3563344
- Our work on Almost Correct Invariants got accepted in ISSTA 2022 (Daejeon, South Korea). https://dl.acm.org/doi/10.1145/3533767.3534381
- Presented our work on Hot Path SSA in Sixth LLVM Performance Workshop at CGO 2020 (Seoul, South Korea) : Sixth LLVM Performance Workshop at CGO-2022
- Profile-guided optimizations made easy - The Hot Path SSA Form in LLVM (LLVM MeetUp)
- Verification of Programs with Concealed Components, SPLASH 2022, Doctoral Symposium.
- Almost Correct Invariants: Synthesizing Inductive Invariants by Fuzzing Proofs, ISSTA 2022
- LLVM MeetUp Talk on Hot Path SSA
- Presented our work on Hot Path SSA in Sixth LLVM Performance Workshop at CGO (Seoul, South Korea)
Slack Campus Lead: https://slackcommunity.com/u/mbhef9/#/about
