☰ Ashutosh Gupta

Course: CS 433 Courses

I am a faculty member in the department of computer science and engineering at IIT Bombay, since early 2018. I received my Ph.D. in computer science from TUM in 2011. During my PhD, I was affiliated with TUM, MPI-SWS, and EPFL at different times. Between the PhD and current position, I was a faculty member at TIFR, Mumbai and post-doctoral researcher in Henzinger group at IST Austria.

Courses

Contact

Email: (initial of first name)k(initial of last name) (at) iitb (dot) ac (dot) in
Office: 320 New CSE building, IIT Bombay, Powai, 400076, Mumbai, India
Phone(Office): +91 22 2576 7724 (avoid calling; preferably write email)

Research interests

• Formal verification: building model checkers for verification of sequential and concurrent software
• Modelling: modelling of biological systems
• Constraint solving: constraint logic programming, decision procedures, and automated theorem proving

Verification Tools

• VAJRA
• HSF
• InvGen

Publications

1. M. Afzal, A. Gupta, and S Akshay, Using Counterexamples to Improve Robustness Verification in Neural Networks,, ATVA 2023
2. M. Afzal, A. Gupta, S. Gambhir, Krishna S, A. Trivedi, and A. Velasquez, LTL-Based Non-Markovian Inverse Reinforcement Learning,, AAMAS 2023
3. P. Abdulla, M. Atig, Krishna S., A. Gupta and O. Tuppe. Optimal Stateless model checking for causal consistency,, TACAS2023
4. K. Dole, J. Komp, A. Gupta, Krisna S. and A. Trivedi. Correct-by-Construction Reinforcement Learning of Cardiac Pacemakers from Duration Calculus Requirements,, AAAI 2023
5. K. Dole, J. Komp, A. Gupta, Krisna S. and A. Trivedi. Event-Triggered and Time-Triggered Duration Calculus for Model-Free Reinforcement Learning,, RTSS 2021
6. A. Biswas, A. Gupta, M. Missula, M. Thattai. Automated inference of production rules for glycans, CMSB 2021 [arXiv].
7. S. Chakraborty, A. Gupta, and D. Unadkat. Diffy: Inductive Reasoning of Array Programs using Difference Invariants, CAV 2021 [arXiv].
8. K. Dole, A. Gupta and Krishna S. Robust Controller Synthesis for Duration Calculus, ATVA 2020 [Springer].
9. M. Afzal, S. Chakraborty, A. Chauhan, B. Chimdyalwar, P. Darke, A. Gupta, S. Kumar, C. Babu M, D. Unadkat, and R. Venkatesh. VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution), TACAS 2020 [IEEE].
10. S. Chakraborty, A. Gupta, and D. Unadkat. Verifying Array Manipulating Programs with Full-Program Induction, TACAS 2020 [arXiv].
11. A. Bhattacharyya,A. Gupta, L. Kuppusamy, S. Mani, A. Shukla, M. Srivas, and M. Thattai, A formal methods approach to predicting new features of the eukaryotic vesicle traffic system [Acta Informatica 2019].
12. A. Gupta, S. Mani, and A. Shukla, Synthesis for vesicle traffic systems, CMSB 2018 [arXiv].
13. A. Gupta, A. Shukla, M. Srivas, and M. Thattai, SMT solving for vesicle traffic systems in cells, SASB 2017 [arXiv].
14. S. Chakraborty, A. Gupta, and D. Unadkat. Verifying Array Manipulating Programs by Tiling, SAS 2017 [arXiv].
15. S. Chakraborty, A. Gupta, and R. Jain. Matching multiplications in Bit-Vector formulas, VMCAI 2017[arXiv].
16. P. Daca, A. Gupta, and T. Henzinger. Abstraction-driven concolic testing, VMCAI 2016 [arXiv].
17. M. Giacobbe, C. Guet, A. Gupta, T. Henzinger, T. Paixao, and T. Petrov. Model Checking Gene Regulatory Networks, (best paper award), TACAS 2015[arXiv].
18. A. Gupta, T. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach. Succinct Representation of Concurrent Trace Sets, POPL 2015[PDF].
19. G. Hofferek and A. Gupta. Suraq - A Controller Synthesis Tool using Uninterpreted Functions, HVC 2014 [PDF].
20. A. Gupta, L. Kovacs, B. Kragl, and A. Voronkov. Extensional Crisis and Proving Identity, ATVA 2014 [PDF].
21. R. Blanc, A. Gupta, L. Kovács, B. Kragl. Tree Interpolation in Vampire, LPAR 2013 .
22. 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].
23. C. Dragoi, A. Gupta, and T. Henzinger. Automatic linearizability proofs of concurrent objects with cooperating updates, CAV 2013 [PDF].
24. A. Gupta. Improved Single Pass Algorithms for Resolution Proof Reduction, ATVA2012 [Full paper] [SAT'12 poster].
25. C. Guet, A. Gupta, T. Henzinger, M. Mateescu, A. Sezgin. Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits, CAV 2012 [PDF].
26. S. Grebenshchikov, A. Gupta, N. Lopes, C. Popeea, and A. Rybalchenko. HSF(C): A Software Verifier based on Horn Clauses, TACAS 2012(SV-COMP) .
27. A. Gupta, C. Popeea, and A. Rybalchenko. Solving Recursion-Free Horn Clauses over LI+UIF, APLAS 2011 [PDF].
28. A. Gupta, C. Popeea, and A. Rybalchenko. Threader: A Constraint-based Verifier for Multi-Threaded Programs, CAV 2011 [PDF].
29. A. Gupta, C. Popeea, and A. Rybalchenko. Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs, POPL 2011[PDF].
30. A. Gupta, C. Popeea, and A. Rybalchenko. Non-monotonic Refinement of Control Abstraction for Concurrent Programs, ATVA 2010 [PDF].
31. B. Cook, A. Gupta, S. Magill, A. Rybalchenko, J. Simsa, S. Singh, and V. Vafeiadis. Finding heap-bounds for hardware synthesis, FMCAD 2009 [PDF].
32. A. Gupta and A. Rybalchenko. InvGen: An Efficient Invariant Generator, CAV 2009 [PDF].
33. A. Gupta, R. Majumdar, and A. Rybalchenko. From Tests to Proofs, TACAS 2009 (best paper award) [PDF].
34. A. Gupta, T. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu. Proving non-termination, POPL 2008 [PDF].