Mastering the Automated Reasoning that Makes Techology Work

Deepak Kapur's contributions to the realm of automated reasoning


When you send a document to your printer, you expect it will print your file, then stop. Accountants trust that the arithmetic operations behind the formulas on their spreadsheets are
exact. And when radiologists treat patients, they rely on medical equipment to deliver precise doses of radiation. In each case the accuracy of the hardware and software depends on the correct implementation of the algorithms within them.

But who checks to be sure that the associated algorithms and their implementations are correct?

Deepak Kapur, distinguished professor of computer science, does. In his research on automated reasoning, formal methods, and program analysis, Kapur builds computer programs to analyze the behavior of other computer programs that run the high-tech products we use daily to ensure that they work according to specifications. For instance, Kapur showed that the floating-point divide (FDIV) bug found in Intel’s 1994 Pentium chip could have been avoided using automated reasoning methods.

His research, conducted with graduate students and collaborators around the world, includes creating and analyzing algorithms and then implementing them to ensure their efficacy. He has developed software tools that can be applied to engineering challenges ranging from scene analysis based on geometric reasoning to robotics, hardware verification, and software analysis.

The findings are relevant to many companies, including Microsoft, Intel, and NASA, which have published papers referencing Kapur’s work and research results. “This process is beneficial in producing products that can be relied upon, especially in lifecritical applications,” he says.

Perhaps Kapur’s most important contribution to the realm of automated reasoning is linking algebraic and logical reasoning. Sir Tony Hoare, a winner of the Turing Award (the Nobel Prize of computer science) coined the term “invariants associated with programs.” But until recently, there was hardly any connection to the concept of invariants in algebra. In collaboration with his former student Enric Rodriguez-Carbonell, Kapur proved that program invariants that can be expressed in algebraic form are indeed invariants mathematicians had been studying for a long time. Using these insights, Kapur created a method that integrates both types of reasoning for automatically generating invariants needed to ensure that programs run correctly. “These results have been the most satisfying for me because, for a long time, the research community had the impression that these two different areas were not at all related,” comments Kapur.

herbrand-award In recognition of that important finding as well as other contributions to numerous areas of automated reasoning, in 2009 he received the prestigious Herbrand Award (pictured at left) given by the International Conference on Automated Deduction (CADE) to honor an individual who has made distinguished contributions to the field of automated reasoning. The award citation for Kapur recognized “his seminal contributions to several areas of automated deduction including inductive theorem proving, geometry theorem proving, term rewriting, unification theory, integration and combination of decision procedures, lemma and loop invariant generation, as well as his work in computer algebra, which helped to bridge the gap between the two areas.”

Kapur is as committed to teaching as he is to research and often discusses his research with his classes. He conducts undergraduate and graduate courses using a Socratic method designed to engage and challenge students. “My view on teaching is that we’re not only trying to give students knowledge, but we also have to teach them how to really think.” In addition to teaching technical courses, Kapur introduced a new course in 1999 on Social and Ethical Issues in Computing, which he taught for many years. With Roli Varma, a professor in UNM’s School of Public Administration, he has been researching reasons behind low enrollments of underrepresented groups in computer science in the US and contrasting them with high enrollments of women, especially, in India and China and other emerging countries.

And while Kapur teaches the next generation of computer scientists to follow in his footsteps, it’s his own thinking, reasoning, and research that helps keep the software and hardware we use every day working the way it should.