My picture


Fifth year PhD Student @ Indian Institute of Technology Delhi

Co-Founder and Verification Engineer @ COMPILER.AI

[Brief Bio] [Research] [COMPILER.AI] [Publications] [Education and Work] [CV]

Brief Bio

I am a senior research scholar in the Amarnath & Shashi Khosla School of IT at the Indian Institute of Techology Delhi working under the supervision of Dr Sorav Bansal. My research interests are in the areas of programming languages, compilers and formal methods. I am the co-founder of COMPILER.AI, a deep tech startup for developing automated program analysis and verification tools for high-assurance software development. I have obtained my B. Tech. degree from NIT-Kurukshetra and have 7 years of work-experience in organizations including Bharat Electronics Limited and Samsung Research Institute.

If you are passionate about system software building or want to participate in high-impact systems research targeted for new emerging markets, join our research & development team at COMPILER.AI.

We work at the intersection of compilers and formal verification, and so a background in these areas would be great --- but as long as you enjoy hacking together interesting software systems, this prior experience is not necessary and can be learned quickly once you are on board with us. We welcome applications from PhD, Masters, and Bachelors degree holders. We would love to talk to you if you already have research experience in compilers/systems.

You will be an early founding member of the team with a great deal of responsibility, and we can assure you that you will have a lot of fun working with us. We offer competitive salaries and attractive equity in the company for our early team members. Our early team members will form our founding team! If you are interested, please reach out to me over email. You can also visit COMPILER.AI for more details.[Growing Our Team Flyer]


My current research is primarily targeted towrads translation validation based certified compilers. Modern compilers still rely on human-written optimizations and algorithms requiring expertise and time and are very hard to be correct. Formally verifying these compilers is not feasible due to the size and ongoing evolution and modification. Alternatively, translation validation involves constructing a separate validation tool (called as equivalence checker) which, after every run of the compiler, formally verifies the result of compilation.

Another important area that I am deeply interested in is development of automated program analysis tools for verifying properties about the source-code and binary-executable code.


Counterexample-Guided Correlation Algorithm for Translation Validation [pdf]
Shubhani Gupta, Abhishek Rose, Sorav Bansal
Proceedings of the ACM on Programming Languages (OOPSLA), 2020

Enhancing Network-on-Chip Performance by Reusing Trace Buffers [pdf]
Neetu Jindal, Shubhani Gupta, Divya Praneetha Ravipati, Preeti Ranjan Panda, Smruti R. Sarangi
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), April 2020

Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition [pdf]
Shubhani Gupta, Aseem Saxena, Anmol Mahajan, Sorav Bansal
In Theory and Applications of Satisfiability Testing (SAT), 2018

Education and Work


Curriculum Vitae (PDF)