Ashutosh Gupta
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.
See also my complete CV.
Contact
Email: (initial of first name)k(initial of last name) (at) iitb (dot) ac (dot) in
Office: 320, Computing Complex, 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
Publications
-
M. Afzal, A. Gupta, and S Akshay,
Using Counterexamples to Improve Robustness Verification in Neural Networks,, ATVA 2023
-
M. Afzal, A. Gupta, S. Gambhir, Krishna S, A. Trivedi, and A. Velasquez,
LTL-Based Non-Markovian Inverse Reinforcement Learning,, AAMAS 2023
-
P. Abdulla, M. Atig, Krishna S., A. Gupta and O. Tuppe.
Optimal Stateless model checking for causal consistency,, TACAS2023
-
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
-
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
-
A. Biswas, A. Gupta, M. Missula, M. Thattai.
Automated inference of production rules for glycans, CMSB 2021 [arXiv].
-
S. Chakraborty, A. Gupta, and D. Unadkat.
Diffy: Inductive Reasoning of Array Programs using Difference Invariants, CAV 2021 [arXiv].
-
K. Dole, A. Gupta and Krishna S. Robust Controller Synthesis for Duration Calculus, ATVA 2020
[Springer].
-
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].
-
S. Chakraborty, A. Gupta, and D. Unadkat.
Verifying Array Manipulating Programs with Full-Program Induction,
TACAS 2020
[arXiv].
-
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].
-
A. Gupta, S. Mani, and A. Shukla,
Synthesis for vesicle traffic systems,
CMSB 2018
[arXiv].
-
A. Gupta, A. Shukla, M. Srivas, and M. Thattai,
SMT solving for vesicle traffic systems in cells,
SASB 2017 [arXiv].
-
S. Chakraborty, A. Gupta, and D. Unadkat.
Verifying Array Manipulating Programs by Tiling,
SAS 2017 [arXiv].
-
S. Chakraborty, A. Gupta, and R. Jain.
Matching multiplications in Bit-Vector formulas,
VMCAI 2017[arXiv].
-
P. Daca, A. Gupta, and T. Henzinger.
Abstraction-driven concolic testing,
VMCAI 2016 [arXiv].
-
M. Giacobbe, C. Guet, A. Gupta, T. Henzinger, T. Paixao, and T. Petrov.
Model Checking Gene Regulatory Networks,
(best paper award),
TACAS 2015[arXiv].
-
A. Gupta, T. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach.
Succinct Representation of Concurrent Trace Sets,
POPL 2015[PDF].
-
G. Hofferek and A. Gupta.
Suraq - A Controller Synthesis Tool using Uninterpreted Functions,
HVC 2014 [PDF].
-
A. Gupta, L. Kovacs, B. Kragl, and A. Voronkov.
Extensional Crisis and Proving Identity,
ATVA 2014 [PDF].
-
R. Blanc, A. Gupta, L. Kovács, B. Kragl.
Tree Interpolation in Vampire,
LPAR 2013 .
-
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].
-
C. Dragoi, A. Gupta, and T. Henzinger.
Automatic linearizability proofs of concurrent objects with cooperating updates,
CAV 2013 [PDF].
-
A. Gupta.
Improved Single Pass Algorithms for Resolution Proof Reduction,
ATVA2012 [Full paper]
[SAT'12 poster].
-
C. Guet, A. Gupta, T. Henzinger, M. Mateescu, A. Sezgin.
Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits,
CAV 2012 [PDF].
-
S. Grebenshchikov, A. Gupta, N. Lopes, C. Popeea, and A. Rybalchenko.
HSF(C): A Software Verifier based on Horn Clauses,
TACAS 2012(SV-COMP) .
-
A. Gupta, C. Popeea, and A. Rybalchenko.
Solving Recursion-Free Horn Clauses over LI+UIF,
APLAS 2011 [PDF].
-
A. Gupta, C. Popeea, and A. Rybalchenko.
Threader: A Constraint-based Verifier for Multi-Threaded Programs,
CAV 2011 [PDF].
-
A. Gupta, C. Popeea, and A. Rybalchenko.
Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs,
POPL 2011[PDF].
-
A. Gupta, C. Popeea, and A. Rybalchenko.
Non-monotonic Refinement of Control Abstraction for Concurrent Programs,
ATVA 2010 [PDF].
-
B. Cook, A. Gupta, S. Magill, A. Rybalchenko, J. Simsa, S. Singh, and V. Vafeiadis.
Finding heap-bounds for hardware synthesis,
FMCAD 2009 [PDF].
-
A. Gupta and A. Rybalchenko.
InvGen: An Efficient Invariant Generator,
CAV 2009 [PDF].
-
A. Gupta, R. Majumdar, and A. Rybalchenko.
From Tests to Proofs,
TACAS 2009
(best paper award) [PDF].
- A. Gupta, T. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu.
Proving non-termination,
POPL 2008 [PDF].
Last modified: Wed Jun 6 10:41:32 IST 2018