Deepak Kapur
According to our database^{1},
Deepak Kapur
authored at least 192 papers
between 1980 and 2019.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at isni.org
On csauthors.net:
Bibliography
2019
Conditional Congruence Closure over Uninterpreted and Interpreted Symbols.
J. Systems Science & Complexity, 2019
2018
An Efficient Algorithm for Computing Parametric Multivariate Polynomial GCD.
Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation, 2018
2017
Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm.
J. Systems Science & Complexity, 2017
Preface  Special Issue of Selected Extended Papers of IJCAR 2014.
J. Autom. Reasoning, 2017
Connecting Program Synthesis and Reachability: Automatic Program Repair Using TestInput Generation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017
Nonlinear Polynomials, Interpolants and Invariant Generation for System Analysis.
Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation colocated with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), 2017
2016
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF.
Proceedings of the Automated Reasoning  8th International Joint Conference, 2016
2015
Decoding femininity in computer science in India.
Commun. ACM, 2015
An Algorithm to Check Whether a Basis of a Parametric Polynomial System is a Comprehensive Gröbner Basis and the Associated Completion Algorithm.
Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation, 2015
Unification and Matching in Hierarchical Combinations of Syntactic Theories.
Proceedings of the Frontiers of Combining Systems  10th International Symposium, 2015
When Is a Formula a Loop Invariant?
Proceedings of the Logic, Rewriting, and Concurrency, 2015
2014
DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants.
ACM Trans. Softw. Eng. Methodol., 2014
An Abstract Domain to Infer Octagonal Constraints with Absolute Value.
Proceedings of the Static Analysis  21st International Symposium, 2014
Using dynamic analysis to generate disjunctive invariants.
Proceedings of the 36th International Conference on Software Engineering, 2014
On Asymmetric Unification and the Combination Problem in Disjoint Theories.
Proceedings of the Foundations of Software Science and Computation Structures, 2014
2013
An efficient method for computing comprehensive Gröbner bases.
J. Symb. Comput., 2013
An efficient algorithm for computing a comprehensive Gröbner system of a parametric polynomial system.
J. Symb. Comput., 2013
On invariant checking.
J. Systems Science & Complexity, 2013
Hierarchical Combination of Unication Algorithms (Extended Abstract).
Proceedings of the 27th International Workshop on Unification, 2013
Hierarchical Combination.
Proceedings of the Automated Deduction  CADE24, 2013
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.
Proceedings of the Automated Deduction  CADE24, 2013
Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants.
Proceedings of the Theories of Programming and Formal Methods, 2013
Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Maxplus Invariants.
Proceedings of the Automated Reasoning and Mathematics, 2013
Harald Ganzinger's Legacy: Contributions to Logics and Programming.
Proceedings of the Programming Logics  Essays in Memory of Harald Ganzinger, 2013
Elimination Techniques for Program Analysis.
Proceedings of the Programming Logics  Essays in Memory of Harald Ganzinger, 2013
2012
A brief introduction to WenTsun Wu's academic career.
J. Symb. Comput., 2012
Preface.
J. Symb. Comput., 2012
Termination Analysis of Imperative Programs Using Bitvector Arithmetic.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2012
Program Analysis Using QuantifierElimination Heuristics  (Extended Abstract).
Proceedings of the Theory and Applications of Models of Computation, 2012
Using dynamic analysis to discover polynomial and array invariants.
Proceedings of the 34th International Conference on Software Engineering, 2012
A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example.
Proceedings of the FM 2012: Formal Methods, 2012
Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions.
Proceedings of the Computer Security  ESORICS 2012, 2012
Rewriting Induction + Linear Arithmetic = Decision Procedure.
Proceedings of the Automated Reasoning  6th International Joint Conference, 2012
2011
Unification over Distributive Exponentiation (Sub)Theories.
Journal of Automata, Languages and Combinatorics, 2011
Termination Analysis of C Programs Using Compiler Intermediate Languages.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011
Protocol analysis in MaudeNPA using unification modulo homomorphic encryption.
Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011
Computing comprehensive Gröbner systems and comprehensive Gröbner bases simultaneously.
Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2011
2010
Unification modulo a partial theory of exponentiation
Proceedings of the Proceedings 24th International Workshop on Unification, 2010
Shape Analysis with Reference Set Relations.
Proceedings of the Verification, 2010
Idle Port Scanning and Noninterference Analysis of Network Protocol Stacks Using Model Checking.
Proceedings of the 19th USENIX Security Symposium, 2010
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010
A new algorithm for computing comprehensive Gröbner systems.
Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2010
Induction, Invariants, and Abstraction.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010
2009
An Algorithm for Computing a Gröbner Basis of a Polynomial Ideal over a Ring with Zero Divisors.
Mathematics in Computer Science, 2009
CayleyDixon projection operator for multiunivariate composed polynomials.
J. Symb. Comput., 2009
Operational Termination of Conditional Rewriting with Builtin Numbers and Semantic Data Structures.
Electr. Notes Theor. Comput. Sci., 2009
Termination of ContextSensitive Rewriting with BuiltIn Numbers and Collection Data Structures.
Proceedings of the Functional and Constraint Logic Programming, 2009
Identification of logically related heap regions.
Proceedings of the 8th International Symposium on Memory Management, 2009
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs.
Proceedings of the Automated Deduction, 2009
2008
Dependency Pairs for Rewriting with BuiltIn Numbers and Semantic Data Structures.
Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008
Sharing analysis of arrays, collections, and recursive structures.
Proceedings of the 8th ACM SIGPLANSIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2008
Identification of HeapCarried Data Dependence Via Explicit Store Heap Models.
Proceedings of the Languages and Compilers for Parallel Computing, 2008
Efficient ContextSensitive Shape Analysis with Graph Based Heap Models.
Proceedings of the Compiler Construction, 17th International Conference, 2008
Multivariate Resultants in Bernstein Basis.
Proceedings of the Automated Deduction in Geometry  7th International Workshop, 2008
2007
Automatic generation of polynomial invariants of bounded degree using abstract interpretation.
Sci. Comput. Program., 2007
Generating all polynomial invariants in simple loops.
J. Symb. Comput., 2007
Heap analysis in the presence of collection libraries.
Proceedings of the 7th ACM SIGPLANSIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2007
Dependency Pairs for Rewriting with Nonfree Constructors.
Proceedings of the Automated Deduction, 2007
2006
Preface on the contributed papers.
J. Symb. Comput., 2006
Bruno Buchberger  A life devoted to symbolic computation.
J. Symb. Comput., 2006
A QuantifierElimination Based Heuristic for Automatically Generating Inductive Assertions for Programs.
J. Systems Science & Complexity, 2006
Third Special Issue on Techniques for Automated Termination Proofs.
J. Autom. Reasoning, 2006
Interpolation for data structures.
Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2006
Inductive Decidability Using Implicit Induction.
Proceedings of the Logic for Programming, 2006
A Static Heap Analysis for Shape and Connectivity: Unified Memory Analysis: The Base Framework.
Proceedings of the Languages and Compilers for Parallel Computing, 2006
Conditions for determinantal formula for resultant of a polynomial system.
Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2006
2005
Preface.
J. Autom. Reasoning, 2005
Preface.
J. Autom. Reasoning, 2005
Towards Dynamic Partitioning of Reactive System Behavior: A Train Controller Case Study.
Proceedings of the Reliable Systems on Unreliable Networked Platforms, 2005
Automatically Generating Loop Invariants Using Quantifier Elimination.
Proceedings of the Deduction and Applications, 23.28. October 2005, 2005
CayleyDixon Resultant Matrices of Multiunivariate Composed Polynomials.
Proceedings of the Computer Algebra in Scientific Computing, 8th International Workshop, 2005
A Unification Algorithm for Analysis of Protocols with Blinded Signatures.
Proceedings of the Mechanizing Mathematical Reasoning, 2005
2004
Resultants for unmixed bivariate polynomial systems produced using the Dixon formulation.
J. Symb. Comput., 2004
Constructing Sylvestertype resultant matrices using the Dixon formulation.
J. Symb. Comput., 2004
Preface.
J. Autom. Reasoning, 2004
Preface.
J. Autom. Reasoning, 2004
Preface.
J. Autom. Reasoning, 2004
An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants.
Proceedings of the Static Analysis, 11th International Symposium, 2004
Automatic generation of polynomial loop.
Proceedings of the Symbolic and Algebraic Computation, 2004
Support hull: relating the cayleydixon resultant constructions to the support of a polynomial system.
Proceedings of the Symbolic and Algebraic Computation, 2004
Program Verification Using Automatic Generation of Invariants.
Proceedings of the Theoretical Aspects of Computing, 2004
2003
Exact resultants for cornercut unmixed multivariate polynomial systems using the Dixon formulation.
J. Symb. Comput., 2003
Announcement.
J. Autom. Reasoning, 2003
On the relationship between the Dixonbased resultant construction and the supports of polynomial systems.
ACM SIGSAM Bulletin, 2003
Automatic Generation of Generalization Lemmas for Proving Properties of TailRecursive Definitions.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003
An Eunification Algorithm for Analyzing Protocols That Use Modular Exponentiation.
Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003
Model Checking Reconfigurable Processor Configurations for Safety Properties.
Proceedings of the Field Programmable Logic and Application, 13th International Conference, 2003
Deciding Inductive Validity of Equations.
Proceedings of the Automated Deduction  CADE19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003
Automatic Generation of Simple Lemmas from Recursive Definitions Using Decision Procedures  Preliminary Report.
Proceedings of the Advances in Computing Science, 2003
2002
On the efficiency and optimality of Dixonbased resultant methods.
Proceedings of the Symbolic and Algebraic Computation, 2002
A Rewrite Rule Based Framework for Combining Decision Procedures.
Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002
2001
Designing a Controller for a MultiTrain MultiTrack System.
Electr. Notes Theor. Comput. Sci., 2001
Dependency Pairs for Equational Rewriting.
Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001
A Survey: Applying Formal Methods to a Software Intensive System.
Proceedings of the 6th IEEE International Symposium on HighAssurance Systems Engineering (HASE 2001), 2001
Decidable Classes of Inductive Theorems.
Proceedings of the Automated Reasoning, First International Joint Conference, 2001
Rewriting, Induction and Decision Procedures: A Case Study of Presburger Arithmetic.
Proceedings of the Symbolic Algebraic Methods and Verification Methods, 2001
2000
Using an induction prover for verifying arithmetic circuits.
STTT, 2000
Conditions for exact resultants using the Dixon formulation.
Proceedings of the 2000 International Symposium on Symbolic and Algebraic Computation, 2000
Extending Decision Procedures with Induction Schemes.
Proceedings of the Automated Deduction, 2000
1998
Transformational Methodology for Proving Termination of Logic Programs.
J. Log. Program., 1998
Mechanical Verification of Adder Circuits using Rewrite Rule Laboratory.
Formal Methods in System Design, 1998
Geometric, Algebraic, and Thermophysical Techniques for Object Recognition in IR Imagery.
Computer Vision and Image Understanding, 1998
Proving AssociativeCommunicative Termination Using RPOCompatible Orderings.
Proceedings of the Automated Deduction in Classical and NonClassical Logics, 1998
IBDL: A Language for Interface Behavior Specification and Testing.
Proceedings of the 4th USENIX Conference on ObjectOriented Technologies and Systems (COOTS), 1998
Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover.
Proceedings of the Advances in Computing Science, 1998
1997
Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification.
Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997
A Total, Ground path Ordering for Proving Termination of ACRewrite Systems.
Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997
Shostak's Congruence Closure as Completion.
Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997
Extraneous Factors in the Dixon Resultant Formulation.
Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation, 1997
Synthesizing Controllers for Hybrid Systems.
Proceedings of the Hybrid and RealTime Systems, 1997
Mechanizing Verification of Arithmetic Circuits: SRT Division.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1997
1996
New Uses of Linear Arithmetic in Automated Theorem Proving by Induction.
J. Autom. Reasoning, 1996
Sparsity Considerations in Dixon Resultants.
Proceedings of the TwentyEighth Annual ACM Symposium on the Theory of Computing, 1996
Distributed Larch Prover (DLP): An Experiment in Parallelizing a RewriteRule Based Prover.
Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996
RewriteBased Automated Reasoning: Challenges Ahead.
Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996
Automating Proofs of Integrity Constraints in Situation Calculus.
Proceedings of the Foundations of Intelligent Systems, 9th International Symposium, 1996
Parallel User Interfaces for Parallel Applications.
Proceedings of the 5th International Symposium on High Performance Distributed Computing (HPDC '96), 1996
Mechanically Verifying a Family of Multiplier Circuits.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996
Lemma Discovery in Automated Induction.
Proceedings of the Automated Deduction  CADE13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996
Automating Induction over Mutually Recursive Functions.
Proceedings of the Algebraic Methodology and Software Technology, 1996
Automated Geometric Reasoning: Dixon Resultants, Gröbner Bases, and Characteristic Sets.
Proceedings of the Automated Deduction in Geometry, 1996
Using Elimination Methods to Compute Thermophysical Algebraic Invariants from Infrared Imagery.
Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, 1996
1995
A Path Ordering for Proving Termination of AC Rewrite Systems.
J. Autom. Reasoning, 1995
Comparison of Various Multivariate Resultant Formulations.
Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, 1995
Maximal Extensions os Simplification Orderings.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1995
Automated Reasoning About Parallel Algorithms Using Powerlists.
Proceedings of the Algebraic Methodology and Software Technology, 1995
1994
An Overview of the Tecton Proof System.
Theor. Comput. Sci., 1994
An Automated Tool for Analyzing Completeness of Equational Specifications.
Proceedings of the 1994 International Symposium on Software Testing and Analysis, 1994
Algebraic and Geometric Reasoning Using Dixon Resultants.
Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1994
Using Linear Arithmetic Procedure for Generating Induction Schemes.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1994
1993
Proving Termination of GHC Programs.
Proceedings of the Logic Programming, 1993
1992
Complexity of Unification Problems with AssociativeCommutative Operators.
J. Autom. Reasoning, 1992
Doubleexponential Complexity of Computing a Complete Set of ACUnifiers
Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992
The Tecton Proof System.
Proceedings of the Formal Methods in Databases and Software Engineering, 1992
Rewriting Concepts in the Study of Termination of Logic Programs.
Proceedings of the ALPUK92, Proceedings of the 4th UK Conference on Logic Programming, London, 30 March, 1992
1991
Automating Inductionless Induction Using Test Sets.
J. Symb. Comput., 1991
SufficientCompleteness, GroundReducibility and their Complexity.
Acta Inf., 1991
The Tecton Proof System.
Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991
Modeling generic polyhedral objects with constraints.
Proceedings of the IEEE Computer Society Conference on Computer Vision and Pattern Recognition, 1991
A Transformational Methodology for Proving Termination of Logic Programs.
Proceedings of the Computer Science Logic, 5th Workshop, 1991
A Case Study of the Completion Procedure: Proving Ring Commutativity Problems.
Proceedings of the Computational Logic  Essays in Honor of Alan Robinson, 1991
1990
On GroundConfluence of Term Rewriting Systems
Inf. Comput., May, 1990
Unnecessary Inferences in AssociativeCommutative Completion Procedures.
Mathematical Systems Theory, 1990
Inference Rules and Proof Procedures for Inequations.
J. Log. Program., 1990
Refutational Proofs of Geometry Theorems via Characteristic Set Computation.
Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1990
A New Method for Proving Termination of ACRewrite Systems.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1990
1989
Consider Only General Superpositions in Completion Procedures.
Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989
An Overview of Rewrite Rule Laboratory (RRL).
Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989
1988
Computability and Implementability Issues in Abstract Data Types.
Sci. Comput. Program., 1988
Only Prime Superpositions Need be Considered in the KnuthBendix Completion Procedure.
J. Symb. Comput., 1988
Computing a Gröbner Basis of a Polynomial Ideal over a Euclidean Domain.
J. Symb. Comput., 1988
Proving Equivalence of Different Axiomatizations of Free Groups.
J. Autom. Reasoning, 1988
Opening the ACUnification Race.
J. Autom. Reasoning, 1988
Wu's Method and its Application to Perspective Viewing.
Artif. Intell., 1988
Geometric Reasoning and Artificial Intelligence: Introduction to the Special Volume.
Artif. Intell., 1988
A Refutational Approach to Geometry Theorem Proving.
Artif. Intell., 1988
A MultiLevel Geometric Reasoning System for Vision.
Artif. Intell., 1988
SemiUnification.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1988
A Mechanizable Induction Principle for Equational Specifications.
Proceedings of the 9th International Conference on Automated Deduction, 1988
FirstOrder Theorem Proving Using Conditional Rewrite Rules.
Proceedings of the 9th International Conference on Automated Deduction, 1988
RRL: A Rewrite Rule Laboratory.
Proceedings of the 9th International Conference on Automated Deduction, 1988
GEOMETER: A Theorem Prover for Algebraic Geometry.
Proceedings of the 9th International Conference on Automated Deduction, 1988
1987
Matching, unification and complexity.
ACM SIGSAM Bulletin, 1987
Proof by Consistency.
Artif. Intell., 1987
On SufficientCompleteness and Related Properties of Term Rewriting Systems.
Acta Inf., 1987
Reasoning in Systems of Equations and Inequations.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1987
1986
Using Gröbner Bases to Reason About Geometry Problems.
J. Symb. Comput., 1986
Inductive Reasoning with Incomplete Specifications (Preliminary Report)
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986
Geometry theorem proving using Hilbert's Nullstellensatz.
Proceedings of the SYMSAC 1986, 1986
Complexity of SufficientCompleteness.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1986
RRL: A Rewrite Rule Laboratory.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986
Proof by Induction Using Test Sets.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986
NPCompleteness of the Set Unification and Matching Problems.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986
1985
The ChurchRosser Property and Special Thue Systems.
Theor. Comput. Sci., 1985
A Finite Thue System with Decidable Word Problem and without Equivalent Finite Canonical System.
Theor. Comput. Sci., 1985
An O(T3) Algorithm for Testing the ChurchRosser Property of Thue Systems.
Theor. Comput. Sci., 1985
The KnuthBendix Completion Procedure and Thue Systems.
SIAM J. Comput., 1985
WorstCase Choice for the Stable Marriage Problem.
Inf. Process. Lett., 1985
A Rewrite Rule Based Approach for Synthesizing Abstract Data Types.
Proceedings of the Mathematical Foundations of Software Development, 1985
A Path Ordering for Proving Termination of Term Rewriting Systems.
Proceedings of the Mathematical Foundations of Software Development, 1985
An IdealTheoretic Approach to Work Problems and Unification Problems over Finitely Presented Commutative Algebras.
Proceedings of the Rewriting Techniques and Applications, First International Conference, 1985
Complexity of Matching Problems.
Proceedings of the Rewriting Techniques and Applications, First International Conference, 1985
An Equational Approach to Theorem Proving in FirstOrder Predicate Calculus.
Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, 1985
Reasoning about three dimensional space.
Proceedings of the 1985 IEEE International Conference on Robotics and Automation, 1985
1984
Algorithms for Computing Groebner Bases of Polynomial Ideals over Various Euclidean Rings.
Proceedings of the EUROSAM 84, 1984
A Natural Proof System Based on rewriting Techniques.
Proceedings of the 7th International Conference on Automated Deduction, 1984
1983
On Proving Uniform Termination and Restricted Termination of Rewriting Systems.
SIAM J. Comput., 1983
1982
Derived Pairs, Overlap Closures, and Rewrite Dominoes: New Tools for Analyzing Term rewriting Systems.
Proceedings of the Automata, 1982
Rewrite Rule Theory and Abstract Data Type Analysis.
Proceedings of the Computer Algebra, 1982
1981
Operators and algebraic structures.
Proceedings of the 1981 conference on Functional programming languages and computer architecture, 1981
Tecton: A Language for Manipulating Generic Objects.
Proceedings of the Program Specification, 1981
1980
Expressiveness of the Operation Set of a Data Abstraction.
Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980