Deepak Kapur, 277-3112
September 20, 2001
UNM Professor receives two NSF Grants totaling more than
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. Kapurs 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
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: firstname.lastname@example.org
of New Mexico
Public Affairs Department
Hodgin Hall, 2nd floor
Albuquerque, NM 87131-0011
Telephone: (505) 277-5813
Fax: (505) 277-1981