Ashutosh K Gupta Ashutosh Gupta

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


Last modified: Wed Sep 10 18:07:24 CEST 2014