Deepak Kapur, 277-3112
Michael Padilla, 277-1816

September 20, 2001

UNM Professor receives two NSF Grants totaling more than $750,000

Deepak Kapur, professor and chair of the Computer Science Department at the University of New Mexico, was recently awarded a three-year, $401,523 grant from the Information Technology Research (ITR) Program of the National Science Foundation (NSF). Out of 1,295 proposals submitted to the program, only 10 percent were funded. Kapur will develop automated tools to help with glitches with software and computer chips.

Kapur, in collaboration with Professor Chris Lynch of Clarkson University and Professor Paliath Narendran of the University at Albany, was also awarded a three-year grant totaling $360,000 (for all three institutions) by the Division of Computer and Communication Research (CCR) of the NSF. Under this grant Kapur will collaborate on developing new algorithms for semantic unification and equation solving, and their application to analysis of cryptographic protocols.

For the ITR grant, Kapur will develop an automated tool that integrates proof methods for induction into automated decision procedures which have been found useful by the hardware industry in finding bugs in chips. Kapur said he first became interested in this application of his research on automated reasoning when a major bug was found in an Intel Pentium chip in 1994 which could have cost Intel more $500 million dollars. Kapur’s research involves checking the circuit behavior expressed as a mathematical property against the circuit description. This is a continuation of his research in formal methods and associated tools for ensuring hardware and software reliability.

The collaborative (CCR) grant is a continuation of research on the theory of semantic unification as well as the design, development and implementation of semantic unification algorithms.

Kapur said semantic unification has been effectively employed in many subfields of logic, computer science, artificial intelligence and cognitive science, with its most popular use being in resolution theorem proving, logic programming languages such as Prolog, and the type inference mechanism in the programming language ML. Semantic unification played a pivotal role in settling open questions in mathematics.

Kapur was earlier awarded a contract for $75,000 from the Office of Naval Research on a related topic to help Dr. Catherine Meadows, a scientist at the Naval Research Laboratory, further develop a tool called NRL Protocol Analyzer. This tool has been used to find bugs in many well-known cryptographic protocols.

Kapur is also the editor-in-chief of the Journal of Automated Reasoning, the premier international journal on automated deduction.


Please let us know what you thought of this article. Comments to:

The University of New Mexico
Public Affairs Department
Hodgin Hall, 2nd floor
Albuquerque, NM 87131-0011
Telephone: (505) 277-5813
Fax: (505) 277-1981