Ashutosh K Gupta Ashutosh Gupta

I am a faculty member in the School of Technology and Computer Science at the Tata Institute of Fundamental Research, Mumbai, since November, 2014. I received my Ph.D. in computer science from TUM in 2011. My Ph.D. adviser was Andrey Rybalchenko. During my PhD, I was affiliated with TUM, MPI-SWS, and EPFL at different times. Between the PhD and current position, I was a post-doctoral researcher in Henzinger group at IST Austria.

See also my complete CV.


Email: (initial of first name)(last name) (at) tifr (dot) res (dot) in
Office: A-211
Mail: TIFR, Homi bhaba road, Colaba, 400005 Mumbai, India
Phone(Office): +91 22 2278 2273 (avoid calling, preferably send email.)
Fax: Please send the document via email

Research interests

Verification Tools


  1. P. Daca, A. Gupta, T. Henzinger. Abstraction-driven concolic testing VMCAI 2016 .
  2. M. Giacobbe, C. Guet, A. Gupta, T. Henzinger, T. Paixao, and T. Petrov. Model Checking Gene Regulatory Networks (best paper award), TACAS 2015[arXiv].
  3. A. Gupta, T. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach. Succinct Representation of Concurrent Trace Sets, POPL 2015[PDF].
  4. G. Hofferek and A. Gupta. Suraq - A Controller Synthesis Tool using Uninterpreted Functions, HVC 2014 [PDF].
  5. A. Gupta, L. Kovacs, B. Kragl, and A. Voronkov. Extensional Crisis and Proving Identity, ATVA 2014 [PDF].
  6. R. Blanc, A. Gupta, L. Kovács, B. Kragl. Tree Interpolation in Vampire, LPAR 2013 .
  7. 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].
  8. C. Dragoi, A. Gupta, and T. Henzinger. Automatic linearizability proofs of concurrent objects with cooperating updates, CAV 2013 [PDF].
  9. A. Gupta. Improved Single Pass Algorithms for Resolution Proof Reduction, ATVA2012 [Full paper] [SAT'12 poster].
  10. C. Guet, A. Gupta, T. Henzinger, M. Mateescu, A. Sezgin. Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits, CAV 2012 [PDF].
  11. S. Grebenshchikov, A. Gupta, N. Lopes, C. Popeea, and A. Rybalchenko. HSF(C): A Software Verifier based on Horn Clauses, TACAS 2012(SV-COMP) .
  12. A. Gupta, C. Popeea, and A. Rybalchenko. Solving Recursion-Free Horn Clauses over LI+UIF, APLAS 2011 [PDF].
  13. A. Gupta, C. Popeea, and A. Rybalchenko. Threader: A Constraint-based Verifier for Multi-Threaded Programs, CAV 2011 [PDF].
  14. A. Gupta, C. Popeea, and A. Rybalchenko. Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs, POPL 2011[PDF].
  15. A. Gupta, C. Popeea, and A. Rybalchenko. Non-monotonic Refinement of Control Abstraction for Concurrent Programs, ATVA 2010 [PDF].
  16. B. Cook, A. Gupta, S. Magill, A. Rybalchenko, J. Simsa, S. Singh, and V. Vafeiadis. Finding heap-bounds for hardware synthesis, FMCAD 2009 [PDF].
  17. A. Gupta and A. Rybalchenko. InvGen: An Efficient Invariant Generator, CAV 2009 [PDF].
  18. A. Gupta, R. Majumdar, and A. Rybalchenko. From Tests to Proofs, TACAS 2009 (best paper award) [PDF].
  19. A. Gupta, T. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu. Proving non-termination, POPL 2008 [PDF].



Last modified: Sun Nov 1 03:02:21 IST 2015