Deepak Kapur
PhD (1980), Massachusetts Institute of
Technology (MIT), Cambridge, MA;
M. Tech. (1973) and B. Tech. (1971),
Indian Institute of Technology (IIT),
Kanpur, India.
Chair, Department of Computer Science, University of New Mexico, Jan. 1999--June 2006.
Visting Professor,
Institute of Software Science, Chinese Academy of Sciences, Beijing, China, 2016 onwards.
Visting Professor,
Dept. of Computer Science and Engineering, Indian Institute of Technology (IIT), Delhi, India, 2012 onwards.
Adjunct Professor,
School of Technology and Computer Science, Tata Institute of Fundamental
Research, Mumbai, India, 2003 onwards.
Professor, Department of Computer Science, Jan. 1988-- Dec. 1998, University at Albany.
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.
Member, Editorial Board,
Journal of Automated
Reasoning. Former Editor-in-Chief (1993-2007).
Member, Editorial Board,
Journal of Symbolic Computation.
Member, Advisory Board,
Theory and Practice of Logic Programming
Editor,
Applicable
Algebra in Engineering, Communication and Computer Science
Editor,
Journal of Systems Science and Complexity
Member of the Editorial Board,
LIPIcs: Leibniz International Proceedings in Informatics
Board Member,
United Nations University - International Institute for Software Technology (UNU-IIST), Macau.
Board Member,
United Nations University - Computing and Society (UNU-CS), Macau.
Research interests
automated reasoning,
term rewriting, formal methods, program analysis,
algebraic and geometric reasoning,
elimination methods, resultants, constraint solving, distributed computing, and social
aspects of computing.
Herbrand Award, 2009.
School of Engineering
Research Excellence Award, UNM, 2010.
Excellence in Research Award, SUNY, Albany, 1998.
PhD Theses supervised
Hengjun Zhao (2015),
Assistant Professor, Southwest University, Chongqing, China.
ThanhVu H. Nguyen (2014),
Assistant Professor, Univ. of Nebraska, Lincoln.
Stephan Falke (2009),
Postdoctoral fellow, Karlsruhe Institute of Technology, Germany.
Mark Marron (2008),
Microsoft Research, Redmond.
Arthur Chtcherba (2003), Google.
Tushar Saxena (1996), BBN Technologies, Cambridge, MA.
Mahadevan Subramaniam (1996), Associate Professor,
University of Nebraska, Omaha, NA.
Hantao Zhang (1988), Professor, Computer Science, University of Iowa.
Abdelilah Kandri-Rody (1984), Professor,
Mathematics, Marakech University, Marakesh, Morrocco.
Books
Theoretical Aspects of Computing - 14th International
Colloquium, ICTAC 2016
Proceedings. Hanoi, Vietnam, October 23-27, 2017.
Lecture Notes in Computer Science 10580,
Springer Verlag, Heidelberg, Germany.
Dang Van Hung and Deepak Kapur (eds.)
Dependable Software Engineering: Theories, Tools, and Applications - Second International
Symposium, SETTA 2016
Proceedings. Beijing, China, November 9-11, 2016.
Lecture Notes in Computer Science 9984,
Springer Verlag, Heidelberg, Germany.
Martin Fraenzle, Deepak Kapur, Naijun Zhan (eds.)
Automated Reasoning - 7th International Joint Conferencef, IJCAR 2014
Proceedings.
Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014.
Lecture Notes in Computer Science 8562, Springer 2014.
Stephane Demri, Deepak Kapur, Christoph Weidenbach (eds.)
Computer Mathematics: 8th Asian Symposium. ASCM (2007)
Proc. of the revised and invited papers, Singapore, Dec. 2007.
Lecture Notes in Artificial Intelligence 5081,
Springer Verlag, Heidelberg, Germany.
Deepak Kapur (ed.)
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.
Deepak 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
Comprehensive Groebner basis Theory for a Parametric Polynomial Ideal and the associated Completion Algorithm
Deepak Kapur
J. of System Science and Complexity , 26(3) 2013, 470-482.
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, and Mingshuai Chen
Proc. Intl. Joint Conf. on Automated Reasoning-- IJCAR 2016 , Springer LNCS 9706, 195-212.
Decoding Femininity in Computer Science in India
Roli Varma and Deepak Kapur
Communication of the ACM , Vol. 58(50), 56-62, 2015.
When is a Formula a Loop Invariant?
S. Falke and D. Kapur
Logic, Rewriting and Concurrency--Festschrift for Jos\'e Meseguer , LNCS 9200, Springer, Sept. 2015, 264-286.
An Algorithm to Check whether a Basis of a Parametric Polynomial System is a ComprehensiveGroebner basis and the associated Completion Algorithm
D. Kapur and Y. Yang
Intl. Symp. on Symbolic and Algebraic Computation (ISSAC) Bristol, July 2015.
DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants
T.V. Nguyen, D. Kapur, W. Weimer, and S. Forrest,
ACM Transactions on Software Engg and Methodology (TOSEM) , 23(4), 2014.
An Efficient Method for Computing Comprehensive Groebner bases
D. Kapur, Y. Sun and D. Wang
J. of Symbolic Computation , 52, May 2013, 124-142.
A Brief Introduction to Wen-Tsun Wu's Academic Career
X.-S. Gao and D. Kapur
J. of Symbolic Computation, 47 (6), June 2012.
Unification over Distributive Exponentiation (Sub)
S. Erbatur, A. M. Marshall D. Kapur, and P. Narendran
Journal of Automata, Languages and Combinatorics, 16(2-4), 2011, 109-140.
A New Algorithm for Computing Comprehensive Groebner Systems
Deepak Kapur, Yao Sun, and Dingkang Wang.
Proc. Intl. Symp on Symbolic and Algebraic Computation (ISSAC), Munich, July 2010.
Unification modulo a Partial Theory of Exponentiation
Deepak Kapur, Andrew Marshall, and Paliath Narendran
Proc. UNIF 2010, Edinburgh, July 2010.
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Stephan Falke, and Deepak Kapur.
Proc. 22nd Intl. Conf. on Automated Deduction (CADE),
Montreal, Canada, August 2009, Springer LNAI 5653.
Identification of Logically related Heap Regions
Mark Marron, Deepak Kapur, and Manuel Hermenegildo
Proc. 2009 Intl. Symp. on Memory Management (ISMM),
Dublin, Ireland, June 2009.
Dependency Pairs for Rewriting with Built-in Numbers and Semantic Data Structures
Stephan Falke, and Deepak Kapur.
Proc. 19th Intl. Conf. on Rewriting Techniques and Applications (RTA),
Hegenberg, Austria, August, 2008. Springer LNCS 5117.
Sharing Analysis of Arrays, Collection, and Recursive Structures
Mark Marron, Mario Mendez-Lojo, Manuel Hermenegildo, Darko Stefanovic, and Deepak Kapur
Proc. 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools
and Engineering (PASTE),
Atlanta, US, 2008.
Efficient Context-Sensitive Shape Analysis with Graph based Heap Models
Mark Marron, Manuel Hermenegildo, Deepak Kapur, and Darko Stefanovic
Proc. Compiler Construction (CC),
Budapest, Hungary, April 2008.
Dependency Pairs for Rewriting with Non-Free Constructors
Stephan Falke, and Deepak Kapur.
Proc. 21st Intl. Conf. on Automated Deduction (CADE), Bremen, Germany, July 2007.
Springer LNAI 4603.
Inductive Decidability using Implicit Induction
Stephan Falke and Deepak Kapur
Proc. 13th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR),
Phnom Penh, Cambodia, Nov. 2006. Springer LNAI 4246.
A Static Heap Analysis for Shape and Connectivity
Mark Marron, Deepak Kapur, , Darko Stefanovic, and Manuel Hermenegildo
Proc. 19th Intl. Workshop on Languages and Compilers for Parallel Computing (LCPC),
New Orleans, USA, Nov. 2006.
Interpolation for Data Structures.
Deepak Kapur, Rupak Majumdar, and Calogero Zarba
Proc. 14th ACM SIGSOFT Intl. Symp on Foundations of Software Engg. (FSE),
Portland, Oregon, Nov. 2006.
A Reduction Approach to Decision Procedures.
Deepak Kapur and Calogero Zarba
2005.
An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants
Enric Rodriguez-Carbonell and Deepak Kapur
Proc. Static Analysis Symposium (SAS), Italy, August 2004.
Automatically Generating Loop Invariants using Quantifier Elimination
Deepak Kapur
Proc. IMACS Intl. Conf. on Applications of Computer Algebra (ACA),
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),
Spain, July 2004.
Decidable Classes of Inductive Theorems
Juergen Giesl and Deepak Kapur
Proc. Intl. Joint Conf. on Atuomated Reasoning (IJCAR),
June 2001, Siena, Italy, 469-484. Springer LNAI 2083.
Extending Decision Procedures with Induction Schemes
Deepak Kapur and Mahadevan Subramaniam
Proc. Intl. Conf. on Atuomated Deduction (CADE), , 2000,
June 2000, 324-345. Springer LNAI 1831.
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),,
Valencia, Spain, June 2003.
Using an Induction Prover for Verifying Arithmetic Circuits
Deepak Kapur and Mahadevan Subramaniam
J. of Software Tools for Technology Transfer.
Vol. 3, No. 1, Sep. 2000, 32-65.
Dependency Pairs for Equational Rewriting
Juergen Giesl and Deepak Kapur
Proc. Intl. Conf. on Rewriting Techniques and Applications (RTA)
May 2001, Utrecht, the Netherlands. Springer LNCS 2051.
Proving Associative-Commutative Termination Using RPO-compatible Orderings
Deepak Kapur and G. Sivakumar
Proc. Automated Deduction in Classical and Non-Classical Logics
Jan 2000. Springer LNAI 1761.
Shostak's Congruence Closure as Completion
Deepak Kapur
International Conference on Rewriting Techniques
and Applications (RTA)
June 1997, Barcelona, Spain, 23-37. Springer LNCS 1232.
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.
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.
Efficiency and Optimality Considerations
of Dixon-based Resultant Methods
Arthur Chtcherba and Deepak Kapur
Intl. Symp on Symbolic and Algebraic Computation (ISSAC)),
France, July 2002.
Conditions for Exact Resultants
using the Dixon Formulation
Arthur Chtcherba and Deepak Kapur
Intl. Symp on Symbolic and Algebraic Computation (ISSAC),
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 (ADG) , 1998. Springer LNAI 1360.
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,
Vol. 72, No. 1, Oct. 1998, 84-97.
List of Selected Publications
Comparative Analysis of Brain Drain, Brain Circulation and Brain Retain: A Case Study of
Indian Institutes of Technology
R. Varma and D. Kapur
Journal of Comparative Policy Analysis, 15(4), 315-330, 2013.
On Invariant Checking
Z. Zhang and D. Kapur
J. of System Science and Complexity, 26(3), 2013, 470-482.
A Resultant
Formula for Multi-univariate Composed Polynomial Systems,
Arthur Chtcherba, Deepak Kapur, Manfred Minimair.
J. of Symbolic Computation, Vol. 44, 2009, 972-999.
Generating all polynomial invariants in simple loops,
Enric Rodriguez-Carbonell and Deepak Kapur
J. of Symbolic Computation, 2007.
Automatic generation of polynomial invariants of
bounded degree using abstract interpretation,
Enrice Rodriguez-Carbonell and Deepak Kapur
J. of Science of Programming, Vol. 64, No. 1, 2007, 54-75.
A Quantifier Elimination based Heuristic for Automatically Generating
Inductive Assertions for Programs,
Deepak Kapur
J. of Systems Science and Complexity, VOl. 19, No. 3, 2006, 307-330.
Induction and Decision Procedures,
Deepak Kapur, Juergen Giesl and Mahadevan Subramaniam
Rev. R. Acad. Cien. Serie A.M. Mat. , Spain, 2004.
Resultants for unmixed bivariate polynomial system
using the Dixon formulation
Arthur Chtcherba and Deepak Kapur
J. of Symbolic Computation, Vol. 38, No. 2, 2004, 915-958
Constructing Sylvester-type resultant
matrices using the Dixon formulation
Arthur Chtcherba and Deepak Kapur
J. of Symbolic Computation, Vol. 38, No. 1, 2004, 774-814.
Exact resultants for corner-cut
unmixed multivariate polynomial systems using the Dixon formulation
Arthur Chtcherba and Deepak Kapur
J. of Symbolic Computation, Vol. 36, Nos. 3-4, 2003, 289-315
Confronting socialization barrier
Cross-ethnic differences in undergraduate women's preference for IT education
Roli Varma, Amit Prasad, and Deepak Kapur
Women and Information Technology: Research on Under-representation
Cohoon and Aspray (eds.), MIT Press, 2006, 301-323.
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,
Vol. 29, No. 2, 1995, 91-114.
An Overview of the Tecton Proof System
Deepak Kapur, David Musser and Xumin Nie
Theoretical Computer Science,
Vol. 133, October, 1994, 307-339.
A Rewrite Rule based Framework for Combining Decision Procedures
Deepak Kapur
Invited Talk,
Fourth International Workshop on Frontiers of Combining Systems (FROCOS)
April 2002, Santa Margherita, Italy, 87-102. Springer LNCS 2309.
Theorem Proving Support for Hardware Verification
Deepak Kapur
Invited Talk, Third Intl. Workshop on First-Order Theorem Proving (FTP)
St. Andrews, Scotland, July 2000.
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 Mahadevan Subramaniam
Invited Talk, Proc. 17th FSTTCS , Kharagpur, India,
Dec. 1997, 103-122. Springer LNCS 1346.
Model Checking Reconfigurable Processor Configurations for Safety Properties
John Cochran, Deepak Kapur and Darko Stefanovic
Proc. Intl. Conf on FPL and Applications,,
Lisbon, Portugal, Sep. 2003.
New Uses of Linear Arithmetic in Automated Theorem Proving by
Induction
Deepak Kapur and Mahadevan Subramaniam
Special issue on Mathematical Induction, J. of Automated Reasoning
, 1996.
Lemma Discovery in Automating Induction
Deepak Kapur and Mahadevan Subramaniam
13th Intl. Conf. on Automated Deduction (CADE),
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
Pascal Van Hentenryck, David 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), Philadelphia, PA, May, 1996.
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 Klaus Madlener
Computers and Mathematics (1989), MIT, Cambridge, June 1989.
Constructors can be Partial Too
Deepak Kapur
Essays in Honor of Larry Wos, Veroff (ed.), MIT Press, 1997.
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 Winter, and Ray 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.
How to contact me