| 2022 | ISSAC | Algorithms for Testing Membership in Univariate Quadratic Modules over the Reals. | Weifeng Shang, Chenqi Mou, Deepak Kapur |
| 2021 | FOSSACS | Interpolation and Amalgamation for Arrays with MaxDiff. | Silvio Ghilardi, Alessandro Gianola, Deepak Kapur |
| 2021 | FSCD | A Modular Associative Commutative (AC) Congruence Closure Algorithm. | Deepak Kapur |
| 2020 | CADE | Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols. | Franz Baader, Deepak Kapur |
| 2019 | CADE | NIL: Learning Nonlinear Interpolants. | Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan |
| 2018 | ISSAC | An Efficient Algorithm for Computing Parametric Multivariate Polynomial GCD. | Deepak Kapur, Dong Lu, Michael B. Monagan, Yao Sun, Dingkang Wang |
| 2017 | ISSAC | Nonlinear Polynomials, Interpolants and Invariant Generation for System Analysis. | Deepak Kapur |
| 2017 | TACAS | Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation. | ThanhVu Nguyen, Westley Weimer, Deepak Kapur, Stephanie Forrest |
| 2016 | CADE | Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. | Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen |
| 2015 | ISSAC | An Algorithm to Check Whether a Basis of a Parametric Polynomial System is a Comprehensive Grbner Basis and the Associated Completion Algorithm. | Deepak Kapur, Yiming Yang |
| 2014 | FOSSACS | On Asymmetric Unification and the Combination Problem in Disjoint Theories. | Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Catherine Meadows, Paliath Narendran, Christophe Ringeissen |
| 2014 | ICSE | Using dynamic analysis to generate disjunctive invariants. | ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest |
| 2014 | SAS | An Abstract Domain to Infer Octagonal Constraints with Absolute Value. | Liqian Chen, Jiangchao Liu, Antoine Min, Deepak Kapur, Ji Wang |
| 2013 | CADE | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. | Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse |
| 2013 | CADE | Hierarchical Combination. | Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen |
| 2012 | CADE | Rewriting Induction + Linear Arithmetic = Decision Procedure. | Stephan Falke, Deepak Kapur |
| 2012 | ESORICS | Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. | Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse |
| 2012 | FM | A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example. | Hengjun Zhao, Naijun Zhan, Deepak Kapur, Kim G. Larsen |
| 2012 | ICSE | Using dynamic analysis to discover polynomial and array invariants. | ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest |
| 2012 | TAMC | Program Analysis Using Quantifier-Elimination Heuristics - (Extended Abstract). | Deepak Kapur |
| 2011 | ISSAC | Computing comprehensive Grbner systems and comprehensive Grbner bases simultaneously. | Deepak Kapur, Yao Sun, Dingkang Wang |
| 2011 | PPDP | Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. | Santiago Escobar, Deepak Kapur, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Ralf Sasse |
| 2010 | CADE | Induction, Invariants, and Abstraction. | Deepak Kapur |
| 2010 | ISSAC | A new algorithm for computing comprehensive Grbner systems. | Deepak Kapur, Yao Sun, Dingkang Wang |
| 2010 | ITP | Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. | Joe Hendrix, Deepak Kapur, Jos Meseguer |
| 2010 | VMCAI | Shape Analysis with Reference Set Relations. | Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur |
| 2009 | CADE | A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. | Stephan Falke, Deepak Kapur |
| 2008 | CC | Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models. | Mark Marron, Manuel V. Hermenegildo, Deepak Kapur, Darko Stefanovic |
| 2007 | CADE | Dependency Pairs for Rewriting with Non-free Constructors. | Stephan Falke, Deepak Kapur |
| 2006 | ISSAC | Conditions for determinantal formula for resultant of a polynomial system. | Arthur D. Chtcherba, Deepak Kapur |
| 2006 | LPAR | Inductive Decidability Using Implicit Induction. | Stephan Falke, Deepak Kapur |
| 2005 | CASC | Cayley-Dixon Resultant Matrices of Multi-univariate Composed Polynomials. | Arthur D. Chtcherba, Deepak Kapur, Manfred Minimair |
| 2004 | ICTAC | Program Verification Using Automatic Generation of Invariants. | Enric Rodrguez-Carbonell, Deepak Kapur |
| 2004 | ISSAC | Support hull: relating the cayley-dixon resultant constructions to the support of a polynomial system. | Arthur D. Chtcherba, Deepak Kapur |
| 2004 | ISSAC | Automatic generation of polynomial loop. | Enric Rodrguez-Carbonell, Deepak Kapur |
| 2004 | SAS | An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants. | Enric Rodrguez-Carbonell, Deepak Kapur |
| 2003 | CADE | Deciding Inductive Validity of Equations. | Jrgen Giesl, Deepak Kapur |
| 2003 | FPL | Model Checking Reconfigurable Processor Configurations for Safety Properties. | John Cochran, Deepak Kapur, Darko Stefanovic |
| 2002 | ISSAC | On the efficiency and optimality of Dixon-based resultant methods. | Arthur D. Chtcherba, Deepak Kapur |
| 2001 | CADE | Decidable Classes of Inductive Theorems. | Jrgen Giesl, Deepak Kapur |
| 2000 | CADE | Extending Decision Procedures with Induction Schemes. | Deepak Kapur, Mahadevan Subramaniam |
| 2000 | ISSAC | Conditions for exact resultants using the Dixon formulation. | Arthur D. Chtcherba, Deepak Kapur |
| 1997 | ISSAC | Extraneous Factors in the Dixon Resultant Formulation. | Deepak Kapur, Tushar Saxena |
| 1996 | AAAI | Using Elimination Methods to Compute Thermophysical Algebraic Invariants from Infrared Imagery. | Jonathan D. Michel, Nagaraj Nandhakumar, Tushar Saxena, Deepak Kapur |
| 1996 | CADE | Lemma Discovery in Automated Induction. | Deepak Kapur, Mahadevan Subramaniam |
| 1996 | CAV | Mechanically Verifying a Family of Multiplier Circuits. | Deepak Kapur, Mahadevan Subramaniam |
| 1996 | HPDC | Parallel User Interfaces for Parallel Applications. | Mark T. Vandevoorde, Deepak Kapur |
| 1996 | ISMIS | Automating Proofs of Integrity Constraints in Situation Calculus. | Leopoldo E. Bertossi, Javier Pinto, Pablo Sez, Deepak Kapur, Mahadevan Subramaniam |
| 1996 | STOC | Sparsity Considerations in Dixon Resultants. | Deepak Kapur, Tushar Saxena |
| 1995 | ISSAC | Comparison of Various Multivariate Resultant Formulations. | Deepak Kapur, Tushar Saxena |
| 1994 | ISSAC | Algebraic and Geometric Reasoning Using Dixon Resultants. | Deepak Kapur, Tushar Saxena, Lu Yang |
| 1994 | ISSTA | An Automated Tool for Analyzing Completeness of Equational Specifications. | Deepak Kapur |
| 1993 | ICLP | Proving Termination of GHC Programs. | M. R. K. Krishna Rao, Deepak Kapur, R. K. Shyamasundar |
| 1992 | LICS | Double-exponential Complexity of Computing a Complete Set of AC-Unifiers | Deepak Kapur, Paliath Narendran |
| 1991 | CSL | A Transformational Methodology for Proving Termination of Logic Programs. | M. R. K. Krishna Rao, Deepak Kapur, R. K. Shyamasundar |
| 1991 | CVPR | Modeling generic polyhedral objects with constraints. | Van-Duc Nguyen, Joseph L. Mundy, Deepak Kapur |
| 1990 | ISSAC | Refutational Proofs of Geometry Theorems via Characteristic Set Computation. | Deepak Kapur, H. K. Wan |
| 1988 | CADE | GEOMETER: A Theorem Prover for Algebraic Geometry. | David Cyrluk, Richard M. Harris, Deepak Kapur |
| 1988 | CADE | RRL: A Rewrite Rule Laboratory. | Deepak Kapur, Hantao Zhang |
| 1988 | CADE | First-Order Theorem Proving Using Conditional Rewrite Rules. | Hantao Zhang, Deepak Kapur |
| 1988 | CADE | A Mechanizable Induction Principle for Equational Specifications. | Hantao Zhang, Deepak Kapur, Mukkai S. Krishnamoorthy |
| 1986 | CADE | NP-Completeness of the Set Unification and Matching Problems. | Deepak Kapur, Paliath Narendran |
| 1986 | CADE | Proof by Induction Using Test Sets. | Deepak Kapur, Paliath Narendran, Hantao Zhang |
| 1986 | CADE | RRL: A Rewrite Rule Laboratory. | Deepak Kapur, G. Sivakumar, Hantao Zhang |
| 1986 | ISSAC | Geometry theorem proving using Hilbert's Nullstellensatz. | Deepak Kapur |
| 1986 | LICS | Inductive Reasoning with Incomplete Specifications (Preliminary Report) | Deepak Kapur, David R. Musser |
| 1985 | IJCAI | An Equational Approach to Theorem Proving in First-Order Predicate Calculus. | Deepak Kapur, Paliath Narendran |
| 1985 | ICRA | Reasoning about three dimensional space. | Deepak Kapur, Joseph L. Mundy, David R. Musser, Paliath Narendran |
| 1984 | CADE | A Natural Proof System Based on rewriting Techniques. | Deepak Kapur, Balakrishnan Krishnamurthy |
| 1982 | ICALP | Derived Pairs, Overlap Closures, and Rewrite Dominoes: New Tools for Analyzing Term rewriting Systems. | John V. Guttag, Deepak Kapur, David R. Musser |
| 1981 | FM | Tecton: A Language for Manipulating Generic Objects. | Deepak Kapur, David R. Musser, Alexander A. Stepanov |
| 1980 | POPL | Expressiveness of the Operation Set of a Data Abstraction. | Deepak Kapur, Mandayam K. Srivas |