Ashutosh 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.

Available research positions



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

Research interests

Verification Tools


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

Last modified: Mon Jun 19 17:38:16 IST 2017