Ashutosh Gupta

Ashutosh Gupta

I am a faculty member in the department of computer science and engineering at IIT Bombay, since early 2018. I received my Ph.D. in computer science from TUM in 2011. During my PhD, I was affiliated with TUM, MPI-SWS, and EPFL at different times. Between the PhD and current position, I was a faculty member at TIFR, Mumbai and post-doctoral researcher in Henzinger group at IST Austria.

See also my complete CV.

Participate in the third Indian SAT+SMT school

Available research positions



Email: (initial of first name)k(initial of last name) (at) iitb (dot) ac (dot) in
Office: 320 New CSE building
Mail: IIT Bombay, Powai, 400076, Mumbai, India
Phone(Office): +91 22 2576 7724 (avoid calling; preferably write email)
Fax: Please send the document via email

Research interests

Verification Tools


  1. S. Chakraborty, A. Gupta, and D. Unadkat. Verifying Array Manipulating Programs with Full-Program Induction, TACAS 2020 .
  2. A. Bhattacharyya,A. Gupta, L. Kuppusamy, S. Mani, A. Shukla, M. Srivas, and M. Thattai, A formal methods approach to predicting new features of the eukaryotic vesicle traffic system [Acta Informatica 2019].
  3. A. Gupta, S. Mani, and A. Shukla, Synthesis for vesicle traffic systems, CMSB 2018 [arXiv].
  4. A. Gupta, A. Shukla, M. Srivas, and M. Thattai, SMT solving for vesicle traffic systems in cells, SASB 2017 [arXiv].
  5. S. Chakraborty, A. Gupta, and D. Unadkat. Verifying Array Manipulating Programs by Tiling, SAS 2017 [arXiv].
  6. S. Chakraborty, A. Gupta, and R. Jain. Matching multiplications in Bit-Vector formulas, VMCAI 2017[arXiv].
  7. P. Daca, A. Gupta, and T. Henzinger. Abstraction-driven concolic testing, VMCAI 2016 [arXiv].
  8. M. Giacobbe, C. Guet, A. Gupta, T. Henzinger, T. Paixao, and T. Petrov. Model Checking Gene Regulatory Networks, (best paper award), TACAS 2015[arXiv].
  9. A. Gupta, T. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach. Succinct Representation of Concurrent Trace Sets, POPL 2015[PDF].
  10. G. Hofferek and A. Gupta. Suraq - A Controller Synthesis Tool using Uninterpreted Functions, HVC 2014 [PDF].
  11. A. Gupta, L. Kovacs, B. Kragl, and A. Voronkov. Extensional Crisis and Proving Identity, ATVA 2014 [PDF].
  12. R. Blanc, A. Gupta, L. Kovács, B. Kragl. Tree Interpolation in Vampire, LPAR 2013 .
  13. G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, and R. Bloem. Synthesizing Multiple Boolean Functions using Interpolation on a Single Proof, FMCAD 2013 [arXiv].
  14. C. Dragoi, A. Gupta, and T. Henzinger. Automatic linearizability proofs of concurrent objects with cooperating updates, CAV 2013 [PDF].
  15. A. Gupta. Improved Single Pass Algorithms for Resolution Proof Reduction, ATVA2012 [Full paper] [SAT'12 poster].
  16. C. Guet, A. Gupta, T. Henzinger, M. Mateescu, A. Sezgin. Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits, CAV 2012 [PDF].
  17. S. Grebenshchikov, A. Gupta, N. Lopes, C. Popeea, and A. Rybalchenko. HSF(C): A Software Verifier based on Horn Clauses, TACAS 2012(SV-COMP) .
  18. A. Gupta, C. Popeea, and A. Rybalchenko. Solving Recursion-Free Horn Clauses over LI+UIF, APLAS 2011 [PDF].
  19. A. Gupta, C. Popeea, and A. Rybalchenko. Threader: A Constraint-based Verifier for Multi-Threaded Programs, CAV 2011 [PDF].
  20. A. Gupta, C. Popeea, and A. Rybalchenko. Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs, POPL 2011[PDF].
  21. A. Gupta, C. Popeea, and A. Rybalchenko. Non-monotonic Refinement of Control Abstraction for Concurrent Programs, ATVA 2010 [PDF].
  22. B. Cook, A. Gupta, S. Magill, A. Rybalchenko, J. Simsa, S. Singh, and V. Vafeiadis. Finding heap-bounds for hardware synthesis, FMCAD 2009 [PDF].
  23. A. Gupta and A. Rybalchenko. InvGen: An Efficient Invariant Generator, CAV 2009 [PDF].
  24. A. Gupta, R. Majumdar, and A. Rybalchenko. From Tests to Proofs, TACAS 2009 (best paper award) [PDF].
  25. A. Gupta, T. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu. Proving non-termination, POPL 2008 [PDF].

Last modified: Wed Jun 6 10:41:32 IST 2018