Specifications of Majster's traversable stack and Veloso's traversable stack. - Deepak Kapur (ACM SIGPLAN Notices, 1979)

Expressiveness of the Operation Set of a Data Abstraction. - Deepak Kapur; Mandayam K. Srivas (POPL, 1980)

Tecton: A Language for Manipulating Generic Objects. - Deepak Kapur; David R. Musser; Alexander A. Stepanov 001 (Program Specification, 1981)

Operators and algebraic structures. - Deepak Kapur; David R. Musser; Alexander A. Stepanov 001 (FPCA, 1981)

Rewrite Rule Theory and Abstract Data Type Analysis. - David R. Musser; Deepak Kapur (EUROCAM, 1982)

Derived Pairs, Overlap Closures, and Rewrite Dominoes: New Tools for Analyzing Term rewriting Systems. - John V. Guttag; Deepak Kapur; David R. Musser (ICALP, 1982)

On Proving Uniform Termination and Restricted Termination of Rewriting Systems. - John V. Guttag; Deepak Kapur; David R. Musser (SIAM J. Comput., 1983)

A Natural Proof System Based on rewriting Techniques. - Deepak Kapur; Balakrishnan Krishnamurthy (CADE, 1984)

Algorithms for Computing Groebner Bases of Polynomial Ideals over Various Euclidean Rings. - Abdelilah Kandri-Rody; Deepak Kapur (EUROSAM, 1984)

Reasoning about three dimensional space. - Deepak Kapur; Joseph L. Mundy; David R. Musser; Paliath Narendran (ICRA, 1985)

An Ideal-Theoretic Approach to Work Problems and Unification Problems over Finitely Presented Commutative Algebras. - Abdelilah Kandri-Rody; Deepak Kapur; Paliath Narendran (RTA, 1985)

A Path Ordering for Proving Termination of Term Rewriting Systems. - Deepak Kapur; Paliath Narendran; G. Sivakumar (TAPSOFT, Vol.1, 1985)

A Rewrite Rule Based Approach for Synthesizing Abstract Data Types. - Deepak Kapur; Mandayam K. Srivas (TAPSOFT, Vol.1, 1985)

Worst-Case Choice for the Stable Marriage Problem. - Deepak Kapur; Mukkai S. Krishnamoorthy (Inf. Process. Lett., 1985)

The Knuth-Bendix Completion Procedure and Thue Systems. - Deepak Kapur; Paliath Narendran (SIAM J. Comput., 1985)

An equational approach to theorem proving in first-order predicate calculus. - Deepak Kapur; Paliath Narendran (ACM SIGSOFT Softw. Eng. Notes, 1985)

RRL: theorem proving environment based on rewriting techniques. - Deepak Kapur; G. Sivakumar (ACM SIGSOFT Softw. Eng. Notes, 1985)

An O(|T|3) Algorithm for Testing the Church-Rosser Property of Thue Systems. - Deepak Kapur; Mukkai S. Krishnamoorthy; Robert McNaughton; Paliath Narendran (Theor. Comput. Sci., 1985)

A Finite Thue System with Decidable Word Problem and without Equivalent Finite Canonical System. - Deepak Kapur; Paliath Narendran (Theor. Comput. Sci., 1985)

The Church-Rosser Property and Special Thue Systems. - Deepak Kapur; Paliath Narendran; Mukkai S. Krishnamoorthy; Robert McNaughton (Theor. Comput. Sci., 1985)

NP-Completeness of the Set Unification and Matching Problems. - Deepak Kapur; Paliath Narendran (CADE, 1986)

Proof by Induction Using Test Sets. - Deepak Kapur; Paliath Narendran; Hantao Zhang 001 (CADE, 1986)

RRL: A Rewrite Rule Laboratory. - Deepak Kapur; G. Sivakumar; Hantao Zhang 001 (CADE, 1986)

Complexity of Sufficient-Completeness. - Deepak Kapur; Paliath Narendran; Hantao Zhang 001 (FSTTCS, 1986)

Geometry theorem proving using Hilbert's Nullstellensatz. - Deepak Kapur (SYMSAC, 1986)

Inductive Reasoning with Incomplete Specifications (Preliminary Report) - Deepak Kapur; David R. Musser (LICS, 1986)

Using Gröbner Bases to Reason About Geometry Problems. - Deepak Kapur (J. Symb. Comput., 1986)

Reasoning in Systems of Equations and Inequations. - Chilukuri K. Mohan; Mandayam K. Srivas; Deepak Kapur (FSTTCS, 1987)

On Sufficient-Completeness and Related Properties of Term Rewriting Systems. - Deepak Kapur; Paliath Narendran; Hantao Zhang 001 (Acta Informatica, 1987)

Proof by Consistency. - Deepak Kapur; David R. Musser (Artif. Intell., 1987)

Matching, unification and complexity. - Deepak Kapur; Paliath Narendran (SIGSAM Bull., 1987)

Complexity of Matching Problems. - Dan Benanav; Deepak Kapur; Paliath Narendran (J. Symb. Comput., 1987)

GEOMETER: A Theorem Prover for Algebraic Geometry. - David Cyrluk; Richard M. Harris; Deepak Kapur (CADE, 1988)

RRL: A Rewrite Rule Laboratory. - Deepak Kapur; Hantao Zhang 001 (CADE, 1988)

First-Order Theorem Proving Using Conditional Rewrite Rules. - Hantao Zhang 001; Deepak Kapur (CADE, 1988)

A Mechanizable Induction Principle for Equational Specifications. - Hantao Zhang 001; Deepak Kapur; Mukkai S. Krishnamoorthy (CADE, 1988)

A Multi-Level Geometric Reasoning System for Vision. - Michele Barry; David Cyrluk; Deepak Kapur; Joseph L. Mundy; Van-Duc Nguyen (Artif. Intell., 1988)

A Refutational Approach to Geometry Theorem Proving. - Deepak Kapur (Artif. Intell., 1988)

Geometric Reasoning and Artificial Intelligence: Introduction to the Special Volume. - Deepak Kapur; Joseph L. Mundy (Artif. Intell., 1988)

Wu's Method and its Application to Perspective Viewing. - Deepak Kapur; Joseph L. Mundy (Artif. Intell., 1988)

Opening the AC-Unification Race. - Hans-Jürgen Bürckert; Alexander Herold; Deepak Kapur; Jörg H. Siekmann; Mark E. Stickel; Michael Tepp; Hantao Zhang 001 (J. Autom. Reason., 1988)

Proving Equivalence of Different Axiomatizations of Free Groups. - Deepak Kapur; Hantao Zhang 001 (J. Autom. Reason., 1988)

Computing a Gröbner Basis of a Polynomial Ideal over a Euclidean Domain. - Abdelilah Kandri-Rody; Deepak Kapur (J. Symb. Comput., 1988)

Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure. - Deepak Kapur; David R. Musser; Paliath Narendran (J. Symb. Comput., 1988)

Computability and Implementability Issues in Abstract Data Types. - Deepak Kapur; Mandayam K. Srivas (Sci. Comput. Program., 1988)

A Completion Procedure for Computing a Canonical Basis for a k-Subalgebra. - Deepak Kapur; Klaus Madlener (Computers and Mathematics, 1989)

An Overview of Rewrite Rule Laboratory (RRL). - Deepak Kapur; Hantao Zhang 001 (RTA, 1989)

Consider Only General Superpositions in Completion Procedures. - Hantao Zhang 001; Deepak Kapur (RTA, 1989)

A New Method for Proving Termination of AC-Rewrite Systems. - Deepak Kapur; G. Sivakumar; Hantao Zhang 001 (FSTTCS, 1990)

Refutational Proofs of Geometry Theorems via Characteristic Set Computation. - Deepak Kapur; H. K. Wan (ISSAC, 1990)

Inference Rules and Proof Procedures for Inequations. - Chilukuri K. Mohan; Mandayam K. Srivas; Deepak Kapur (J. Log. Program., 1990)

Unnecessary Inferences in Associative-Commutative Completion Procedures. - Hantao Zhang 001; Deepak Kapur (Math. Syst. Theory, 1990)

On Ground-Confluence of Term Rewriting Systems - Deepak Kapur; Paliath Narendran; Friedrich Otto (Inf. Comput., 1990)

A Case Study of the Completion Procedure: Proving Ring Commutativity Problems. - Deepak Kapur; Hantao Zhang 001 (Computational Logic - Essays in Honor of Alan Robinson, 1991)

Modeling generic polyhedral objects with constraints. - Van-Duc Nguyen; Joseph L. Mundy; Deepak Kapur (CVPR, 1991)

The Tecton Proof System. - Raj Agarwal; David R. Musser; Deepak Kapur; Xumin Nie (RTA, 1991)

Sufficient-Completeness, Ground-Reducibility and their Complexity. - Deepak Kapur; Paliath Narendran; Daniel J. Rosenkrantz; Hantao Zhang 001 (Acta Informatica, 1991)

Automating Inductionless Induction Using Test Sets. - Deepak Kapur; Paliath Narendran; Hantao Zhang 001 (J. Symb. Comput., 1991)

Semi-Unification. - Deepak Kapur; David R. Musser; Paliath Narendran; Jonathan Stillman (Theor. Comput. Sci., 1991)

Rewriting Concepts in the Study of Termination of Logic Programs. - R. K. Shyamasundar; M. R. K. Krishna Rao; Deepak Kapur (ALPUK, 1992)

The Tecton Proof System. - Deepak Kapur; David R. Musser; Xumin Nie (Formal Methods in Databases and Software Engineering, 1992)

Double-exponential Complexity of Computing a Complete Set of AC-Unifiers - Deepak Kapur; Paliath Narendran (LICS, 1992)

Complexity of Unification Problems with Associative-Commutative Operators. - Deepak Kapur; Paliath Narendran (J. Autom. Reason., 1992)

Using Linear Arithmetic Procedure for Generating Induction Schemes. - Deepak Kapur; Mahadevan Subramaniam (FSTTCS, 1994)

Algebraic and Geometric Reasoning Using Dixon Resultants. - Deepak Kapur; Tushar Saxena; Lu Yang (ISSAC, 1994)

An Automated Tool for Analyzing Completeness of Equational Specifications. - Deepak Kapur (ISSTA, 1994)

An Overview of the Tecton Proof System. - Deepak Kapur; Xumin Nie; David R. Musser (Theor. Comput. Sci., 1994)

Automated Reasoning About Parallel Algorithms Using Powerlists. - Deepak Kapur; Mahadevan Subramaniam (AMAST, 1995)

Maximal Extensions os Simplification Orderings. - Deepak Kapur; G. Sivakumar (FSTTCS, 1995)

Comparison of Various Multivariate Resultant Formulations. - Deepak Kapur; Tushar Saxena (ISSAC, 1995)

A Path Ordering for Proving Termination of AC Rewrite Systems. - Deepak Kapur; G. Sivakumar; Hantao Zhang 001 (J. Autom. Reason., 1995)

Using Elimination Methods to Compute Thermophysical Algebraic Invariants from Infrared Imagery. - Jonathan D. Michel; Nagaraj Nandhakumar; Tushar Saxena; Deepak Kapur (AAAI/IAAI, Vol. 2, 1996)

Automated Geometric Reasoning: Dixon Resultants, Gröbner Bases, and Characteristic Sets. - Deepak Kapur (Automated Deduction in Geometry, 1996)

Automating Induction over Mutually Recursive Functions. - Deepak Kapur; Mahadevan Subramaniam (AMAST, 1996)

Lemma Discovery in Automated Induction. - Deepak Kapur; Mahadevan Subramaniam (CADE, 1996)

Mechanically Verifying a Family of Multiplier Circuits. - Deepak Kapur; Mahadevan Subramaniam (CAV, 1996)

Parallel User Interfaces for Parallel Applications. - Mark T. Vandevoorde; Deepak Kapur (HPDC, 1996)

Automating Proofs of Integrity Constraints in Situation Calculus. - Leopoldo E. Bertossi; Javier Pinto; Pablo Sáez; Deepak Kapur; Mahadevan Subramaniam (ISMIS, 1996)

Rewrite-Based Automated Reasoning: Challenges Ahead. - Deepak Kapur (RTA, 1996)

Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover. - Mark T. Vandevoorde; Deepak Kapur (RTA, 1996)

Sparsity Considerations in Dixon Resultants. - Deepak Kapur; Tushar Saxena (STOC, 1996)

New Uses of Linear Arithmetic in Automated Theorem Proving by Induction. - Deepak Kapur; Mahadevan Subramaniam (J. Autom. Reason., 1996)

Mechanizing Verification of Arithmetic Circuits: SRT Division. - Deepak Kapur; Mahadevan Subramaniam (FSTTCS, 1997)

Synthesizing Controllers for Hybrid Systems. - Deepak Kapur; R. K. Shyamasundar (HART, 1997)

Extraneous Factors in the Dixon Resultant Formulation. - Deepak Kapur; Tushar Saxena (ISSAC, 1997)

Shostak's Congruence Closure as Completion. - Deepak Kapur (RTA, 1997)

A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems. - Deepak Kapur; G. Sivakumar (RTA, 1997)

Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification. - Deepak Kapur (TPHOLs, 1997)

Proving Termination of GHC Programs. - M. R. K. Krishna Rao; Deepak Kapur; R. K. Shyamasundar (New Gener. Comput., 1997)

Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover. - Deepak Kapur; Mahadevan Subramaniam (ASIAN, 1998)

IBDL: A Language for Interface Behavior Specification and Testing. - Sreenivasa Viswanadha; Deepak Kapur (COOTS, 1998)

Proving Associative-Communicative Termination Using RPO-Compatible Orderings. - Deepak Kapur; G. Sivakumar (FTP (LNCS Selection), 1998)

Geometric, Algebraic, and Thermophysical Techniques for Object Recognition in IR Imagery. - Jonathan D. Michel; Nagaraj Nandhakumar; Tushar Saxena; Deepak Kapur (Comput. Vis. Image Underst., 1998)

Mechanical Verification of Adder Circuits using Rewrite Rule Laboratory. - Deepak Kapur; Mahadevan Subramaniam (Formal Methods Syst. Des., 1998)

Transformational Methodology for Proving Termination of Logic Programs. - M. R. K. Krishna Rao; Deepak Kapur; R. K. Shyamasundar (J. Log. Program., 1998)

Extending Decision Procedures with Induction Schemes. - Deepak Kapur; Mahadevan Subramaniam (CADE, 2000)

Conditions for exact resultants using the Dixon formulation. - Arthur D. Chtcherba; Deepak Kapur (ISSAC, 2000)

Using an induction prover for verifying arithmetic circuits. - Deepak Kapur; Mahadevan Subramaniam (Int. J. Softw. Tools Technol. Transf., 2000)

Rewriting, Induction and Decision Procedures: A Case Study of Presburger Arithmetic. - Deepak Kapur (Symbolic Algebraic Methods and Verification Methods, 2001)

Decidable Classes of Inductive Theorems. - Jürgen Giesl; Deepak Kapur (IJCAR, 2001)

A Survey: Applying Formal Methods to a Software Intensive System. - Adriaan de Groot; Jozef Hooman; Fabrice Kordon; Emmanuel Paviot-Adet; Isabelle Vernier-Mounier; Michel Lemoine; Gervais Gaudiére; Victor L. Winter; Deepak Kapur (HASE, 2001)

Dependency Pairs for Equational Rewriting. - Jürgen Giesl; Deepak Kapur (RTA, 2001)

Designing a Controller for a Multi-Train Multi-Track System. - Deepak Kapur; Victor L. Winter; Raymond Berg (ATMOS, 2001)

A Rewrite Rule Based Framework for Combining Decision Procedures. - Deepak Kapur (FroCoS, 2002)

On the efficiency and optimality of Dixon-based resultant methods. - Arthur D. Chtcherba; Deepak Kapur (ISSAC, 2002)

Automatic Generation of Simple Lemmas from Recursive Definitions Using Decision Procedures - Preliminary Report. - Deepak Kapur; Mahadevan Subramaniam (ASIAN, 2003)

Deciding Inductive Validity of Equations. - Jürgen Giesl; Deepak Kapur (CADE, 2003)

Model Checking Reconfigurable Processor Configurations for Safety Properties. - John Cochran; Deepak Kapur; Darko Stefanovic (FPL, 2003)

An E-unification Algorithm for Analyzing Protocols That Use Modular Exponentiation. - Deepak Kapur; Paliath Narendran; Lida Wang (RTA, 2003)

Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions. - Deepak Kapur; Nikita A. Sakhanenko (TPHOLs, 2003)

On the relationship between the Dixon-based resultant construction and the supports of polynomial systems. - Arthur D. Chtcherba; Deepak Kapur (SIGSAM Bull., 2003)

Announcement. - Deepak Kapur (J. Autom. Reason., 2003)

Exact resultants for corner-cut unmixed multivariate polynomial systems using the Dixon formulation. - Arthur D. Chtcherba; Deepak Kapur (J. Symb. Comput., 2003)

Formal Specifcation and Refinement of a Safe Train Control Function. - Victor L. Winter; Deepak Kapur; G. Fuehrer (Formal Methods for Embedded Distributed Systems, 2004)

Program Verification Using Automatic Generation of Invariants. - Enric Rodríguez-Carbonell; Deepak Kapur (ICTAC, 2004)

Support hull: relating the cayley-dixon resultant constructions to the support of a polynomial system. - Arthur D. Chtcherba; Deepak Kapur (ISSAC, 2004)

Automatic generation of polynomial loop. - Enric Rodríguez-Carbonell; Deepak Kapur (ISSAC, 2004)

An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants. - Enric Rodríguez-Carbonell; Deepak Kapur (SAS, 2004)

Preface. - Deepak Kapur (J. Autom. Reason., 2004)

Preface. - Deepak Kapur; Laurent Vigneron (J. Autom. Reason., 2004)

Constructing Sylvester-type resultant matrices using the Dixon formulation. - Arthur D. Chtcherba; Deepak Kapur (J. Symb. Comput., 2004)

Resultants for unmixed bivariate polynomial systems produced using the Dixon formulation. - Arthur D. Chtcherba; Deepak Kapur (J. Symb. Comput., 2004)

A Unification Algorithm for Analysis of Protocols with Blinded Signatures. - Deepak Kapur; Paliath Narendran; Lida Wang (Mechanizing Mathematical Reasoning, 2005)

Cayley-Dixon Resultant Matrices of Multi-univariate Composed Polynomials. - Arthur D. Chtcherba; Deepak Kapur; Manfred Minimair (CASC, 2005)

Automatically Generating Loop Invariants Using Quantifier Elimination. - Deepak Kapur (Deduction and Applications, 2005)

Towards Dynamic Partitioning of Reactive System Behavior: A Train Controller Case Study. - Victor L. Winter; Deepak Kapur (Monterey Workshop, 2005)

Preface. - Jürgen Giesl; Deepak Kapur (J. Autom. Reason., 2005)

Conditions for determinantal formula for resultant of a polynomial system. - Arthur D. Chtcherba; Deepak Kapur (ISSAC, 2006)

A Static Heap Analysis for Shape and Connectivity: Unified Memory Analysis: The Base Framework. - Mark Marron; Deepak Kapur; Darko Stefanovic; Manuel V. Hermenegildo (LCPC, 2006)

Inductive Decidability Using Implicit Induction. - Stephan Falke 001; Deepak Kapur (LPAR, 2006)

Interpolation for data structures. - Deepak Kapur; Rupak Majumdar; Calogero G. Zarba (SIGSOFT FSE, 2006)

Third Special Issue on Techniques for Automated Termination Proofs. - Jürgen Giesl; Deepak Kapur (J. Autom. Reason., 2006)

A Quantifier-Elimination Based Heuristic for Automatically Generating Inductive Assertions for Programs. - Deepak Kapur (J. Syst. Sci. Complex., 2006)

Bruno Buchberger - A life devoted to symbolic computation. - Hoon Hong; Deepak Kapur; Peter Paule; Franz Winkler 001 (J. Symb. Comput., 2006)

Preface on the contributed papers. - Deepak Kapur (J. Symb. Comput., 2006)

Dependency Pairs for Rewriting with Non-free Constructors. - Stephan Falke 001; Deepak Kapur (CADE, 2007)

Heap analysis in the presence of collection libraries. - Mark Marron; Darko Stefanovic; Manuel V. Hermenegildo; Deepak Kapur (PASTE, 2007)

Generating all polynomial invariants in simple loops. - Enric Rodríguez-Carbonell; Deepak Kapur (J. Symb. Comput., 2007)

Automatic generation of polynomial invariants of bounded degree using abstract interpretation. - Enric Rodríguez-Carbonell; Deepak Kapur (Sci. Comput. Program., 2007)

Multivariate Resultants in Bernstein Basis. - Deepak Kapur; Manfred Minimair (Automated Deduction in Geometry, 2008)

Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models. - Mark Marron; Manuel V. Hermenegildo; Deepak Kapur; Darko Stefanovic (CC, 2008)

Identification of Heap-Carried Data Dependence Via Explicit Store Heap Models. - Mark Marron; Darko Stefanovic; Deepak Kapur; Manuel V. Hermenegildo (LCPC, 2008)

Sharing analysis of arrays, collections, and recursive structures. - Mark Marron; Mario Méndez-Lojo; Manuel V. Hermenegildo; Darko Stefanovic; Deepak Kapur (PASTE, 2008)

Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures. - Stephan Falke 001; Deepak Kapur (RTA, 2008)

Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures. - Stephan Falke 001; Deepak Kapur (WRS@RTA, 2008)

A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. - Stephan Falke 001; Deepak Kapur (CADE, 2009)

Identification of logically related heap regions. - Mark Marron; Deepak Kapur; Manuel V. Hermenegildo (ISMM, 2009)

Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures. - Stephan Falke 001; Deepak Kapur (WFLP, 2009)

Cayley-Dixon projection operator for multi-univariate composed polynomials. - Arthur D. Chtcherba; Deepak Kapur; Manfred Minimair (J. Symb. Comput., 2009)

An Algorithm for Computing a Gröbner Basis of a Polynomial Ideal over a Ring with Zero Divisors. - Deepak Kapur; Yongyang Cai (Math. Comput. Sci., 2009)

Induction, Invariants, and Abstraction. - Deepak Kapur (IJCAR, 2010)

A new algorithm for computing comprehensive Gröbner systems. - Deepak Kapur; Yao Sun 004; Dingkang Wang (ISSAC, 2010)

Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. - Joe Hendrix; Deepak Kapur; José Meseguer 001 (ITP, 2010)

Idle Port Scanning and Non-interference Analysis of Network Protocol Stacks Using Model Checking. - Roya Ensafi; Jong Chun Park; Deepak Kapur; Jedidiah R. Crandall (USENIX Security Symposium, 2010)

Shape Analysis with Reference Set Relations. - Mark Marron; Rupak Majumdar; Darko Stefanovic; Deepak Kapur (VMCAI, 2010)

Unification modulo a partial theory of exponentiation - Deepak Kapur; Andrew M. Marshall; Paliath Narendran (UNIF, 2010)

Computing comprehensive Gröbner systems and comprehensive Gröbner bases simultaneously. - Deepak Kapur; Yao Sun 004; Dingkang Wang (ISSAC, 2011)

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. - Santiago Escobar 001; Deepak Kapur; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Ralf Sasse (PPDP, 2011)

Termination Analysis of C Programs Using Compiler Intermediate Languages. - Stephan Falke 001; Deepak Kapur; Carsten Sinz (RTA, 2011)

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Ralf Sasse (UNIF, 2011)

Unification over Distributive Exponentiation (Sub)Theories. - Serdar Erbatur; Andrew M. Marshall; Deepak Kapur; Paliath Narendran (J. Autom. Lang. Comb., 2011)

Rewriting Induction + Linear Arithmetic = Decision Procedure. - Stephan Falke 001; Deepak Kapur (IJCAR, 2012)

Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Sonia Santiago; Ralf Sasse (ESORICS, 2012)

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 (FM, 2012)

Using dynamic analysis to discover polynomial and array invariants. - ThanhVu Nguyen; Deepak Kapur; Westley Weimer; Stephanie Forrest (ICSE, 2012)

Program Analysis Using Quantifier-Elimination Heuristics - (Extended Abstract). - Deepak Kapur (TAMC, 2012)

Termination Analysis of Imperative Programs Using Bitvector Arithmetic. - Stephan Falke 001; Deepak Kapur; Carsten Sinz (VSTTE, 2012)

Preface. - Xiao-Shan Gao; Deepak Kapur (J. Symb. Comput., 2012)

A brief introduction to Wen-Tsun Wu's academic career. - Xiao-Shan Gao; Deepak Kapur (J. Symb. Comput., 2012)

Elimination Techniques for Program Analysis. - Deepak Kapur (Programming Logics, 2013)

Harald Ganzinger's Legacy: Contributions to Logics and Programming. - Deepak Kapur; Robert Nieuwenhuis; Andrei Voronkov; Christoph Weidenbach; Reinhard Wilhelm (Programming Logics, 2013)

Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants. - Deepak Kapur; Zhihai Zhang; Matthias Horbach; Hengjun Zhao; Qi Lu; ThanhVu Nguyen (Automated Reasoning and Mathematics, 2013)

Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants. - Hengjun Zhao; Naijun Zhan; Deepak Kapur (Theories of Programming and Formal Methods, 2013)

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Sonia Santiago; Ralf Sasse (CADE, 2013)

Hierarchical Combination. - Serdar Erbatur; Deepak Kapur; Andrew M. Marshall; Paliath Narendran; Christophe Ringeissen (CADE, 2013)

Hierarchical Combination of Unication Algorithms (Extended Abstract). - Serdar Erbatur; Deepak Kapur; Andrew M. Marshall; Paliath Narendran; Christophe Ringeissen (UNIF@RTA/TLCA, 2013)

Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation - Deepak Kapur; Naijun Zhan; Hengjun Zhao (CoRR, 2013)

On invariant checking. - Zhihai Zhang; Deepak Kapur (J. Syst. Sci. Complex., 2013)

An efficient algorithm for computing a comprehensive Gröbner system of a parametric polynomial system. - Deepak Kapur; Yao Sun 004; Dingkang Wang (J. Symb. Comput., 2013)

An efficient method for computing comprehensive Gröbner bases. - Deepak Kapur; Yao Sun 004; Dingkang Wang (J. Symb. Comput., 2013)

On Asymmetric Unification and the Combination Problem in Disjoint Theories. - Serdar Erbatur; Deepak Kapur; Andrew M. Marshall; Catherine Meadows 001; Paliath Narendran; Christophe Ringeissen (FoSSaCS, 2014)

Using dynamic analysis to generate disjunctive invariants. - ThanhVu Nguyen; Deepak Kapur; Westley Weimer; Stephanie Forrest (ICSE, 2014)

An Abstract Domain to Infer Octagonal Constraints with Absolute Value. - Liqian Chen; Jiangchao Liu; Antoine Miné; Deepak Kapur; Ji Wang 001 (SAS, 2014)

On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract). - Serdar Erbatur; Deepak Kapur; Andrew M. Marshall; Catherine Meadows 001; Paliath Narendran; Christophe Ringeissen (UNIF, 2014)

Hierarchical Combination of Matching Algorithms (Extended Abstract). - Serdar Erbatur; Deepak Kapur; Andrew M. Marshall; Paliath Narendran; Christophe Ringeissen (UNIF, 2014)

DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. - ThanhVu Nguyen; Deepak Kapur; Westley Weimer; Stephanie Forrest (ACM Trans. Softw. Eng. Methodol., 2014)

When Is a Formula a Loop Invariant? - Stephan Falke 001; Deepak Kapur (Logic, Rewriting, and Concurrency, 2015)

Unification and Matching in Hierarchical Combinations of Syntactic Theories. - Serdar Erbatur; Deepak Kapur; Andrew M. Marshall; Paliath Narendran; Christophe Ringeissen (FroCos, 2015)

An Algorithm to Check Whether a Basis of a Parametric Polynomial System is a Comprehensive Gröbner Basis and the Associated Completion Algorithm. - Deepak Kapur; Yiming Yang (ISSAC, 2015)

Decoding femininity in computer science in India. - Roli Varma; Deepak Kapur (Commun. ACM, 2015)

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. - Ting Gan; Liyun Dai; Bican Xia; Naijun Zhan; Deepak Kapur; Mingshuai Chen (IJCAR, 2016)

Interpolation synthesis for quadratic polynomial inequalities and combination with textit{EUF}. - Ting Gan; Liyun Dai; Bican Xia; Naijun Zhan; Deepak Kapur; Mingshuai Chen (CoRR, 2016)

Nonlinear Polynomials, Interpolants and Invariant Generation for System Analysis. - Deepak Kapur (SC²@ISSAC, 2017)

Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation. - ThanhVu Nguyen; Westley Weimer; Deepak Kapur; Stephanie Forrest (TACAS (1), 2017)

Preface - Special Issue of Selected Extended Papers of IJCAR 2014. - Stéphane Demri; Deepak Kapur; Christoph Weidenbach (J. Autom. Reason., 2017)

Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm. - Deepak Kapur (J. Syst. Sci. Complex., 2017)

An Efficient Algorithm for Computing Parametric Multivariate Polynomial GCD. - Deepak Kapur; Dong Lu; Michael B. Monagan; Yao Sun 004; Dingkang Wang (ISSAC, 2018)

NIL: Learning Nonlinear Interpolants. - Mingshuai Chen; Jian Wang 042; Jie An 001; Bohua Zhan; Deepak Kapur; Naijun Zhan (CADE, 2019)

Editorial. - Martin Fränzle; Deepak Kapur; Heike Wehrheim; Naijun Zhan (Formal Aspects Comput., 2019)

Conditional Congruence Closure over Uninterpreted and Interpreted Symbols. - Deepak Kapur (J. Syst. Sci. Complex., 2019)

Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols. - Franz Baader; Deepak Kapur (IJCAR (1), 2020)

Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (CILC, 2020)

Compactly Representing Uniform Interpolants for EUF using (conditional) DAGS. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (CoRR, 2020)

An Algorithm for Computing a Minimal Comprehensive Gröbner , Basis of a Parametric Polynomial System. - Deepak Kapur; Yiming Yang (CoRR, 2020)

Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version). - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (CoRR, 2020)

Interpolation and Amalgamation for Arrays with MaxDiff. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (FoSSaCS, 2021)

A Modular Associative Commutative (AC) Congruence Closure Algorithm. - Deepak Kapur (FSCD, 2021)

AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDiff. - José Abel Castellanos Joo; Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (SMT, 2021)

Algorithms for computing greatest common divisors of parametric multivariate polynomials. - Deepak Kapur; Dong Lu; Michael B. Monagan; Yao Sun 004; Dingkang Wang (J. Symb. Comput., 2021)

Algorithms for Testing Membership in Univariate Quadratic Modules over the Reals. - Weifeng Shang; Chenqi Mou; Deepak Kapur (ISSAC, 2022)

General Interpolation and Strong Amalgamation for Contiguous Arrays. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur; Chiara Naso (CoRR, 2022)

Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols. - Franz Baader; Deepak Kapur (J. Autom. Reason., 2022)

Uniform Interpolants in EUF: Algorithms using DAG-representations. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur (Log. Methods Comput. Sci., 2022)

Verifying Quantum Phase Estimation (QPE) using Prove-It. - Wayne M. Witzel; Warren D. Craft; Robert D. Carr; Deepak Kapur (CoRR, 2023)

Existence and Construction of a Gröbner Basis for a Polynomial Ideal. - Deepak Kapur; Paliath Narendran (CoRR, 2023)

Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties. - Deepak Kapur (Log. Methods Comput. Sci., 2023)

Interpolation Results for Arrays with Length and MaxDiff. - Silvio Ghilardi; Alessandro Gianola; Deepak Kapur; Chiara Naso (ACM Trans. Comput. Log., 2023)

Attacking Connection Tracking Frameworks as used by Virtual Private Networks. - Benjamin Mixon-Baca; Jeffrey Knockel; Diwen Xue; Tarun Ayyagari; Deepak Kapur; Roya Ensafi; Jedidiah R. Crandall (Proc. Priv. Enhancing Technol., 2024)

A new algorithm for Gröbner bases conversion. - Amir Hashemi; Deepak Kapur (J. Symb. Comput., 2025)

Computing Certificates of Strictly Positive Polynomials in Archimedean Quadratic Modules. - Weifeng Shang; Chenqi Mou; José Abel Castellanos; Deepak Kapur (CoRR, 2025)