Ashutosh Gupta

Ashutosh Gupta is an Associate Professor in the Department of Computer Science and Engineering at the Indian Institute of Technology Bombay, where he has been a faculty member since 2018. His research focuses on formal methods for software verification, particularly in the areas of model checking, constraint solving, and automated reasoning for both sequential and concurrent programs. He teaches advanced courses including Automated Reasoning (CS433), Analysis of Concurrent Programs (CS766), and Logic for Computer Science (CS228).

Dr. Gupta received his Ph.D. in Computer Science from Technical University of Munich (TUM) in 2011, with affiliations during his doctoral studies at TUM, Max Planck Institute for Software Systems (MPI-SWS), and École Polytechnique Fédérale de Lausanne (EPFL). Prior to joining IIT Bombay, he served as a faculty member at Tata Institute of Fundamental Research (TIFR) in Mumbai and completed post-doctoral research in the Henzinger group at IST Austria.

His research interests span formal verification of sequential and concurrent software, modeling of biological systems, and constraint solving including constraint logic programming, decision procedures, and automated theorem proving. He has developed several verification tools including VAJRA, HSF, and InvGen. His work bridges theoretical foundations with practical applications, particularly in verifying safety-critical systems and biological processes.

Dr. Gupta's publication record shows a consistent trajectory of high-impact research in top venues like POPL, CAV, TACAS, and AAAI. His recent work has expanded into neural network verification, reinforcement learning verification for medical devices, and applying formal methods to biological systems, demonstrating both depth in core verification techniques and breadth in application domains.

• Best Paper Award at TACAS 2015
• Best Paper Award at TACAS 2009

Dr. Gupta actively mentors numerous students through course projects, research presentations, and specialized workshops like SATfest. He has supervised students working on SAT/SMT solvers, verification of concurrent programs, and applications of formal methods to biological systems. His teaching philosophy emphasizes hands-on experience with verification tools and encourages students to engage with cutting-edge research through reading and presenting recent conference papers.

He maintains active research collaborations with institutions including TUM, MPI-SWS, EPFL, IST Austria, and TIFR, reflecting his continued integration into the international formal methods research community.