Ashutosh K Gupta Ashutosh Gupta

I am moving to Tata Institute of Fundamental Research, Mumbai at the position of Reader (equivalent to tenure track asst. professor).

I am a post-doctoral researcher in Henzinger group at IST Austria. 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.

See also my complete CV.


Email: (initial of first name)(last name) (at) ist (dot) ac (dot) at
Office: 01.02.070
Mail: IST Austria, Am campus 1, 3400 Klosterneuburg, Austria
Phone(Office): +43 2243 9000 3512
Fax: Please send the document via email

Research interests

Verification Tools


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


Last modified: Sun Oct 5 14:02:38 CEST 2014