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.

Participate in the second Indian SAT+SMT school

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

Last modified: Mon Sep 18 10:11:04 IST 2017