Carnegie Mellon's Bryant Wins Newton Award for Formal Verification Technology

acm
The Association for Computing Machinery
Advancing Computing as a Science & Profession

Contact: Virginia Gold
212-626-0505
[email protected]

 Printable PDF

NEW YORK, May 19, 2010 – The ACM Special Interest Group on Design Automation (SIGDA) and the Institute of Electrical and Electronics Engineers (IEEE) will present the 2010 ACM/IEEE A. R. Newton Award to Randal E. Bryant for his revolutionary use of mathematical techniques to prove that hardware and software designs function as intended.  Bryant, Dean of the Carnegie Mellon University School of Computer Science, developed efficient algorithms based on Reduced Ordered Binary Decision Diagrams (ROBDDs) to manipulate the logic functions that form the basis for computer designs. These innovations formed the basis of formal verification techniques that could be used to eliminate all flaws from large-scale automated circuit designs for the first time.  The Newton Award, which honors outstanding technical contributions in electronic design automation, is based on the impact of that contribution over a significant period.  It will be presented at the 2010 Design Automation Conference (DAC 2010)  June 13-18, in Anaheim, CA. 

Bryant’s achievement is based on a 1986 paper entitled "Graph-Based Algorithms for Boolean Function Manipulation," published in IEEE Transactions on Computers, Vol. C-35, No. 8.  Until recently, it was the single most cited paper in computer science as measured by Citeseer, the Scientific Literature Digital Library, and currently resides at number 6.  

As early as 1985, Bryant was able to demonstrate that Ordered Binary Decision Diagrams (OBDDs) enable circuits to be simulated symbolically, covering all possible behaviors in a single execution. His technology thus became a catalyst in the growth of formal verification, which has significantly improved the quality of hardware and software design products in the age of increasingly complex computer designs.  OBDDs are now widely used for circuit verification, synthesis, and testing, as well as in such diverse areas as artificial intelligence planning and compiler optimization. Today, formal verification based on Bryant’s OBDDs is applied as standard practice by all major electronic design automation hardware engineers and integrated device manufacturers.

Bryant is a Fellow of ACM and IEEE, as well as a member of the National Academy of Engineering.  In 2007, he received the IEEE Piore Award for outstanding contributions in the field of information processing, in relation to computer science.  He is the recipient of the 1998 ACM Kanellakis Theory and Practice Award (shared with Edmund M. Clarke, Ken McMillan, and E. Allen Emerson) for contributing to the development of symbolic model checking.  He also received the 2009 EDAC/IEEE Kaufman Award for his impact on the electronic design automation field.  In addition, he was awarded the 1989 IEEE W.R.G. Baker Prize for the best paper appearing in any IEEE publication during the preceding year. 

Along with David R. O'Hallaron, Bryant developed a novel approach to teaching about the hardware, networking, and system software that comprise a system from the perspective of an advanced programmer, rather than from those of the system designers.  Their textbook, Computer Systems: A Programmer’s Perspective is now in its second edition, and is in use at more than 130 universities worldwide with translations into Chinese and Russian. 

Bryant has been on the faculty at Carnegie Mellon since 1984, starting as an Assistant Professor and progressing to his current rank of University Professor of Computer Science.  He previously taught at the California Institute of Technology.  He also holds a courtesy appointment in the Electrical and Computer Engineering Department.  A graduate of the University of Michigan, he received his B.S. in Applied Mathematics and his Ph.D. from the Massachusetts Institute of Technology.  

The A. Richard Newton Technical Impact Award in Electronic Design Automation honors A. Richard Newton, a luminary in the design automation area in academia and industry.  He was a faculty contributor and advisor to many of the leaders in the field as well as a company founder, and dean of engineering at the University of California, Berkeley, who died in 2007. Professor Newton embodied the idea of technical impact that this award seeks to recognize.

 About ACM

ACM, the Association for Computing Machinery www.acm.org is the world’s largest educational and scientific computing society, uniting computing educators, researchers and professionals to inspire dialogue, share resources and address the field’s challenges. ACM strengthens the computing profession’s collective voice through strong leadership, promotion of the highest standards, and recognition of technical excellence. ACM supports the professional growth of its members by providing opportunities for life-long learning, career development, and professional networking.  

 About SIGDA

SIGDA, Special Interest Group on Design Automation, www.sigda.org   is ACM's professional development organization for the Electronic Design Automation (EDA) community.  SIGDA is committed to advancing the skills and knowledge of electronic design automation professionals and students throughout the world by sponsoring and organizing international workshops, symposia and conferences, and leading the way in capturing archival electronic design automation publications