November 7, 2005
ECE alumnus Shuvendu Lahiri (M.S. 2001; Ph.D. 2004) won the Outstanding Ph.D. Dissertation Award in Electronic Design Automation from the Association for Computing Machinery Special Interest Group in Design Automation (ACM SIGDA) for his work, "Unbounded System Verification Using Decision Procedure and Predicate Abstraction." Lahiri was advised by Randal Bryant, Dean of the School of Computer Science (SCS) and Professor of CS and ECE, and is now a researcher in the testing, verification, and measurement group at Microsoft Research in Redmond, CA.
He was chosen for the award for his contributions in improving the efficiency and capabilities of predicate abstraction, a method of formally verifying abstract hardware and software designs. The selection committee cited Lahiri's indexed predicate abstraction method as "innovative, substantial and of long-term impact." Giving him a unanimous vote, the judges considered his efforts to be an important part of the research on this subject that has been produced from Bryant's team in recent years.
"Shuvendu surprised the entire world of formal verification research. Building on the base of simple Boolean logic, he was able to create a tool for verifying systems described in abstract forms of mathematical logic," said Bryant. "His tool is much more automated than its predecessors, making it suitable for hardware and software developers without requiring extensive training in logic."
Lahiri received a plaque and check at the opening ceremonies of the International Conference on Computer Aided Design (ICCAD) on November 7 in San Jose. At Microsoft, Lahiri continues to research the development and application of symbolic techniques for making testing and verification more scalable and automated. He is interested in theorem-provers for first-order logic, predicate abstraction and using them to analyze software.
While at Carnegie Mellon, Lahiri was part of the Center for Silicon System Implementation (CSSI) and received a research assistantship from the Semiconductor Research Corporation (SRC). He was a teaching assistant for an undergraduate introductory course on real-time embedded systems and a graduate course on hardware systems engineering. In the summers, Lahiri interned off campus with Microsoft Research and Motorola.