Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Prof. Deepak Kapur's home page
[go: Go Back, main page]

Deepak Kapur




Chair & Professor
Department of Computer Science
School of Engineering
University of New Mexico


PhD (1980), Massachusetts Institute of Technology (MIT), Cambridge, MA;
M. Tech. (1973) and B. Tech. (1971), Indian Institute of Technology (IIT), Kanpur, India.

Professor, Computer Science Dept. 1988-98.
Founder and former Director, Institute for Programming and Logics, University at Albany.

Member, Research Staff, Computer Science Branch, General Electric Corporate Research and Development, Schenectady, NY, 1980-87.



Editor-in-Chief, Journal of Automated Reasoning (see also this)
Member, Advisory Board, Theory and Practice of Logic Programming
Editor, Applicable Algebra in Engineering, Communication and Computer Science
Editor, Constraints Journal

Guest Editor, Special Issue on Logic, Mathematics and Computer Science: Interactions
Journal of Symbolic Computation

Member, Executive Board, Computer Science Research Institute (CSRI), Sandia National Labs.

Member, Executive Committee, Los Alamos Computer Science Institute (LACSI), Los Alamos National Lab.


Research interests:

automated reasoning, term rewriting, formal methods, programming languages, algebraic and geometric reasoning, and their applications in computer vision and solid modeling, elimination methods, constraint solving, and distributed, concurrent and real time systems.

PhD theses supervised:

A. Chtcherba (2003), Assistant Professor, University of Texas--Pan American, Edinburgh, TX.
T. Saxena (1996), BBN Technologies, Cambridge, MA.
M. Subramaniam (1996), Assistant Professor, University of Nebraska, Omaha, NA.
H. Zhang (1988), Professor, Computer Science, University of Iowa.
A. Kandri-Rody (1984), Professor, Mathematics, Marakech University, Marakesh, Morrocco.

Excellence in Research Award, 1998, University at Albany, Albany, NY

Books



Automated Deduction -- CADE-11
Proc. 11th International Conference on Automated Deduction, Saratoga Spring, NY, June 1992,
Lecture Notes in Artificial Intelligence 607, Springer Verlag, Heidelberg, Germany.
D. Kapur (ed.)

Symbolic and Numerical Computation for Artificial Intelligence
Academic Press, 1992.
Bruce Donald, Deepak Kapur, and Joseph L. Mundy (eds.)

Geometric Reasoning
MIT Press, 1989.
Deepak Kapur and Joseph L. Mundy (eds.)

Recent Publications


An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants
Enric Rodriguez-Carbonell and Deepak Kapur
Proc. Static Analysis Symposium, SAS-2004,
Italy, August 2004.

Automatically Generating Loop Invariants using Quantifier Elimination
Deepak Kapur
Proc. IMACS Intl. Conf. on Applications of Computer Algebra, ACA-2004,
Beaumont, Texas, July 2004.

Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations
Enric Rodriguez-Carbonell and Deepak Kapur
Proc. Intl. Symp on Symbolic and Algebraic Computation, ISSAC-2004,
Spain, July 2004.

Decidable Classes of Inductive Theorems
Juergen Giesl and Deepak Kapur
Proc. Intl. Joint Conf. on Atuomated Reasoning (IJCAR),
Springer LNAI 2083, June 2001, Siena, Italy, 469-484.

Extending Decision Procedures with Induction Schemes
Deepak Kapur and Mahadevan Subramaniam
Proc. Intl. Conf. on Atuomated Deduction (CADE-17), , 2000,
Springer LNAI 1831, June 2000, 324-345.

Model Checking Reconfigurable Processor Configurations for Safety Properties
John Cochran, Deepak Kapur and Darko Stefanovic
Proc. Intl. Conf on FPL and Applications, 2003,,
Lisbon, Portugal, Sep. 2003.

Undecidability of Unification over Two Theories of Modular Exponentiation
Deepak Kapur, Paliath Narendran and Lida Wang
Proc. Intl. Workshop on Unification, UNIF-2003,,
Valencia, Spain, June 2003.

An E-unification Algorithm for Analyzing Protocols that Use Modular Exponentiation
Deepak Kapur, Paliath Narendran and Lida Wang
Proc. Intl. Conf on Rewriting Techniques and Applications, RTA-2003,,
Valencia, Spain, June 2003.

Using an Induction Prover for Verifying Arithmetic Circuits
Deepak Kapur and Mahadevan Subramaniam
J. of Software Tools for Technology Transfer.
Springer Verlag, Vol. 3(1), Sep. 2000, 32-65.

Theorem Proving Support for Hardware Verification
Deepak Kapur
Invited Talk, Third Intl. Workshop on First-Order Theorem Proving, FTP 2000
St. Andrews, Scotland, July 2000.

Dependency Pairs for Equational Rewriting
Juergen Giesl and Deepak Kapur
Proc. Intl. Conf. on Rewriting Techniques and Applications (RTA)
Springer LNCS 2051, May 2001, Utrecht, the Netherlands.

Proving Associative-Commutative Termination Using RPO-compatible Orderings
Deepak Kapur and G. Sivakumar
Proc. Automated Deduction in Classical and Non-Classical Logics
Springer LNAI 1761, Jan 2000.

A Rewrite Rule based Framework for Combining Decision Procedures
Deepak Kapur
Invited Talk, Fourth International Workshop on Frontiers of Combining Systems FROCOS'02
Springer LNCS 2309, April 2002, Santa Margherita, Spain, 87-102.

Shostak's Congruence Closure as Completion
Deepak Kapur
International Conference on Rewriting Techniques and Applications, RTA `97
Springer LNCS 1232, June 1997, Barcelona, Spain, 23-37.

Rewriting, Induction and Decision Procedures: A Case Study of Presburger Arithmetic
Deepak Kapur
Symbolic-algebraic Methods and Verification Methods --Theory and Applications
Alefeld, Rohn, Rump and Tamamato (eds), Springer Mathematics, Jan 2001, 129-144.

Efficiency and Optimality Considerations of Dixon-based Resultant Methods
Arthur Chtcherba and Deepak Kapur
Intl. Symp on Symbolic and Algebraic Computation, ISSAC-2002,
France, July 2002.

A Complete Analysis of Resultants and Extraneous Factors for Unmixed Bivariate Polynomial Systems using the Dixon Formulation
Arthur Chtcherba and Deepak Kapur
Eighth Rhine Workshop on Computer Algebra (RWCA'02),
March 2002, Mannheim, Germany.

Conditions for Exact Resultants using the Dixon Formulation
Arthur Chtcherba and Deepak Kapur
Intl. Symp on Symbolic and Algebraic Computation, ISSAC-2000,
St. Andrews, Scotland, Aug 2000.

Extracting Sparse Resultant Matrices from Dixon Resultant Formulation
Arthur Chtcherba and Deepak Kapur
Seventh Rhine Workshop on Computer Algebra (RWCA'00),
March 2000, Bregenz, Austria.

Automated Geometric Reasoning: Dixon Resultants, Groebner bases and Characteristic sets
Deepak Kapur
Automated Deduction in Geometry , Springer LNAI 1360, 1998.

Geometric, Algebraic, and Thermophysical Techniques for Object Recognition in IR Imagery
J.D. Michel, N. Nandhakumar, Tushar Saxena, and Deepak Kapur
Computer Vision and Image Understanding, 72(1), Oct. 1998, 84-97.

IBDL: A Language for Interface Behavior Specification and Testing
Deepak Kapur and Sreenivasa Viswanadha
Proc. 4th Conf. Object-Oriented Technologies and Systems (COOTS'98) ,
Santa Fe, New Mexico, April 1998.

Designing a Controller for a Multi-Train Multi-Track System
Deepak Kapur, Victor L. Winter, and Ray S. Berg
Proc. ICALP 2001 Satellite Workshop on
Algorithmic Methods and Models for Organization of Railways, ATMOS 2001,
Creete,Greece, July 2001.

On the Construction of a Domain Language for a Class of Reactive Systems
Deepak Kapur and Victor L. Winter
High Integrity Software , Kluwer Academic Publishers, 2001, 169-196.

List of Selected Publications



Equation Manipulation
Deepak Kapur
Encyclopedia of Electrical and Electronic Engg.,
(ed. J.G. Webster), John Wiley, 2000, 117-142.

An Overview of Rewrite Rule Laboratory (RRL)
Deepak Kapur and Hantao Zhang
J. of Computer and Mathematics with Applications, 29, 2, 1995, 91-114.

An Overview of the Tecton Proof System
Deepak Kapur, David R. Musser and Xumin Nie
Theoretical Computer Science, Vol. 133, October, 1994, 307-339.

Mechanizing Reasoning about Large Finite Tables in a Rewrite based Theorem Prover
Deepak Kapur and Mahadevan Subramaniam
Proc. ASIAN'98 , Manila, Phillipines, Dec. 1998, 22-42.

Mechanizing Verification of Arithmetic Circuits: SRT Division
Deepak Kapur and M. Subramaniam
Invited Talk, Proc. FSTTCS-17 , Kharagpur, India, Springer LNCS 1346, 103-122, Dec 1997.

New Uses of Linear Arithmetic in Automated Theorem Proving by Induction
Deepak Kapur M. and Subramaniam
Special issue on Mathematical Induction, J. of Automated Reasoning , 1996.

Lemma Discovery in Automating Induction
Deepak Kapur and M. Subramaniam
Intl. Conf. on Automated Deduction, CADE-13, New Jersey, July 1996.

A Refutational Approach to Geometry Theorem Proving
Deepak Kapur
J. of Artificial Intelligence, Vol. 37, Dec. 1988, 61-93.

Double-Exponential Complexity of Computing A Complete Set of AC-unifiers
Deepak Kapur and Paliath Narendran
Logic in Computer Science (LICS), Santa Cruz, CA, June 1992.

Elimination Methods: An Introduction
Deepak Kapur and Lakshman Y.N.
Symbolic and Numerical Computation for Artificial Intelligence,
Donald, Kapur and Mundy (eds.), Academic Press, 1992, 45-87.

Synthesizing Controllers for Hybrid Systems
Deepak Kapur and R.K. Shyamasundar
Intl. Workshop on Hybrid and Real-Time Systems, HART `97,
Springer LNCS 1201, 361-375, Grenoble, France.

Solving Polynomial Systems Using a Branch and Prune Approach
P. Van Hentenryck, D. McAllester and Deepak Kapur
SIAM J. on Numerical Analysis, 34, 2, April 1997, 797-827.

An Approach for Solving Systems of Parametric Polynomial Equations
Deepak Kapur
Principles and Practice of Constraint Programming,
(eds. Saraswat and Van Hentenryck), MIT press, 1995.

Sparsity Considerations in Dixon Resultants
Deepak Kapur and Tushar Saxena
28th Annual ACM Symp. on Theory of Computing, STOC '96, Philadelphia, PA, May, 1996.

Comparison of Various Multivariate Resultant Formulations
Deepak Kapur and Tushar Saxena
International Symposium on Symbolic and Algebraic Computation (ISSAC), Montreal, July 1995.

Algebraic and Geometric Reasoning using Dixon Resultants
Deepak Kapur, Tushar Saxena and Lu Yang
International Symposium on Symbolic and Algebraic Computation (ISSAC), Oxford, July 1994.

A Completion Procedure for Computing a Canonical Basis for a k-Subalgebra
Deepak Kapur and K. Madlener
Computers and Mathematics '89, MIT, Cambridge, June 1989.

Constructors can be Partial Too
Deepak Kapur
Essays in Honor of Larry Wos, (ed: R. Veroff) MIT Press, 1997.

How to contact me