Proving non-termination. - Ashutosh Gupta 001; Thomas A. Henzinger; Rupak Majumdar; Andrey Rybalchenko; Ru-Gang Xu (POPL, 2008)

InvGen: An Efficient Invariant Generator. - Ashutosh Gupta 001; Andrey Rybalchenko (CAV, 2009)

Finding heap-bounds for hardware synthesis. - Byron Cook; Ashutosh Gupta 001; Stephen Magill; Andrey Rybalchenko; Jirí Simsa; Satnam Singh; Viktor Vafeiadis (FMCAD, 2009)

Non-monotonic Refinement of Control Abstraction for Concurrent Programs. - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (ATVA, 2010)

Solving Recursion-Free Horn Clauses over LI+UIF. - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (APLAS, 2011)

Threader: A Constraint-Based Verifier for Multi-threaded Programs. - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (CAV, 2011)

Predicate abstraction and refinement for verifying multi-threaded programs. - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (POPL, 2011)

Constraint solving for verification. - Ashutosh Kumar Gupta 001 (2011)

Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits. - Calin C. Guet; Ashutosh Gupta 001; Thomas A. Henzinger; Maria Mateescu; Ali Sezgin (CAV, 2012)

HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). - Sergey Grebenshchikov; Ashutosh Gupta 001; Nuno P. Lopes; Corneliu Popeea; Andrey Rybalchenko (TACAS, 2012)

Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. - Cezara Dragoi; Ashutosh Gupta 001; Thomas A. Henzinger (CAV, 2013)

From tests to proofs. - Ashutosh Gupta 001; Rupak Majumdar; Andrey Rybalchenko (Int. J. Softw. Tools Technol. Transf., 2013)

Generalised Interpolation by Solving Recursion-Free Horn Clauses - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (HCVS, 2014)

Succinct Representation of Concurrent Trace Sets. - Ashutosh Gupta 001; Thomas A. Henzinger; Arjun Radhakrishna; Roopsha Samanta; Thorsten Tarrach (POPL, 2015)

Model Checking Gene Regulatory Networks. - Mirco Giacobbe; Calin C. Guet; Ashutosh Gupta 001; Thomas A. Henzinger; Tiago Paixão; Tatjana Petrov (TACAS, 2015)

Guest Editors' Introduction to Special Issue on Computational Methods in Systems Biology. - Ashutosh Gupta 001; Thomas A. Henzinger (ACM Trans. Model. Comput. Simul., 2015)

Abstraction-driven Concolic Testing. - Przemyslaw Daca; Ashutosh Gupta 001; Thomas A. Henzinger (VMCAI, 2016)

Verifying Array Manipulating Programs by Tiling. - Supratik Chakraborty; Ashutosh Gupta 001; Divyesh Unadkat (SAS, 2017)

Matching Multiplications in Bit-Vector Formulas. - Supratik Chakraborty; Ashutosh Gupta 001; Rahul Jain 001 (VMCAI, 2017)

Model checking the evolution of gene regulatory networks. - Mirco Giacobbe; Calin C. Guet; Ashutosh Gupta 001; Thomas A. Henzinger; Tiago Paixão; Tatjana Petrov (Acta Informatica, 2017)

VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution). - Mohammad Afzal; Supratik Chakraborty; Avriti Chauhan; Bharti Chimdyalwar; Priyanka Darke; Ashutosh Gupta 001; Shrawan Kumar 001; Charles Babu M; Divyesh Unadkat; R. Venkatesh 001 (TACAS (2), 2020)

Verifying Array Manipulating Programs with Full-Program Induction. - Supratik Chakraborty; Ashutosh Gupta 001; Divyesh Unadkat (TACAS (1), 2020)

Diffy: Inductive Reasoning of Array Programs Using Difference Invariants. - Supratik Chakraborty; Ashutosh Gupta 001; Divyesh Unadkat (CAV (2), 2021)

Full-program induction: verifying array programs sans loop invariants. - Supratik Chakraborty; Ashutosh Gupta 001; Divyesh Unadkat (Int. J. Softw. Tools Technol. Transf., 2022)

Using Counterexamples to Improve Robustness Verification in Neural Networks. - Mohammad Afzal; Ashutosh Gupta 001; S. Akshay 001 (ATVA (1), 2023)

Sensitivity Verification for Additive Decision Tree Ensembles. - Arhaan Ahmad; Tanay Vineet Tayal; Ashutosh Gupta 001; S. Akshay 001 (ICLR, 2025)

Monitoring Robustness and Individual Fairness. - Ashutosh Gupta 001; Thomas A. Henzinger; Konstantin Kueffner; Kaushik Mallik; David Pape (CoRR, 2025)

Glitches in Decision Tree Ensemble Models. - Satyankar Chandra; Ashutosh Gupta 001; Kaushik Mallik; Krishna Shankaranarayanan; Namrita Varshney (CoRR, 2025)