Prof. Deepak Kapur
Biography
Deepak Kapur is a distinguished professor of computer science at University of New Mexico, USA. From 1998 until 2006, he served as the chair of the computer science department there. Kapur got his Ph.D. in computer science in 1980 from MIT. After his Ph.D., he worked at the GE R&D Center in Schenectady, USA from 1980-1987 where he was honored in 1985 for his research contributions to computer science. In 1988, Kapur was hired as a full tenured professor by the State University of New York, Albany, USA. He has held visiting and adjunct positions at RPI, MIT, Max Planck Institute, IBM Research, TIFR, IMEDIA Madrid, IIT Delhi, and the Institute of Software of the Chinese Academy of Sciences. He has served as a consultant to GE R&D, IBM Research, Fujitsu and Sandia National Labs.
Kapur has been conducting research in areas of automated deduction, induction theorem proving, term rewriting, unification theory, formal methods, program analysis, hardware verification, algebraic and geometric reasoning and their applications. His group built one of the first rewrite-based theorem provers, called Rewrite Rule Laboratory. He has co-edited 6 books and published over 200 papers.
Kapur served as the editor-in-chief of the Journal of Automated Reasoning from 1993-2007. He has served on the editorial board of many journals including Journal of Symbolic Computation, as well as on the editorial board of the new open access initiative LIPIcs started in cooperation with Schloss Dagstuhl-Leibniz Center. He also served on the Board of Directors of the United Nations University's International Institute for Software Technology, Macau and later United Nations University's Computing and Society Institute in Macau. In 2009, Kapur received the Herbrand Award for distinguished contributions to automated reasoning.
Abstract
The short course will cover various automated reasoning algorithms the author has used for hardware and software analysis. The main paradigm employed is that of rewrite methods. Completion algorithms and their applications will be explored for generating decision procedures. This will include congruence closure, conditional congruence closure, Groebner basis algorithms and Knuth-Bendix completion procedure and their generalizations for associative-commutative theories as well as first-order predicate calculus with equality. This will be followed by solvers for specific theories, including DPLL and CDCL methods for SAT and SMT methods for quantifier-free theories. In parallel, the use of these algorithms for verifying properties of hardware and software will be illustrated. A particular focus will be on automatically generating loop invariants needed in verifying properties of software. Time permitting and based on audience interest, automated methods for proofs by induction as well as quantifier-elimination based approach for interpolant generation will be explored.