Carnegie Mellon University

Randal Bryant

Randal Bryant

Courtesy Professor, Electrical and Computer Engineering
Professor, Computer Science Department

Download Hi-res Photo
Address 5000 Forbes Avenue
Pittsburgh, PA 15213


Randal E. Bryant is a University Professor in the Computer Science Department at Carnegie Mellon University. He 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 also holds a courtesy appointment in the Electrical and Computer Engineering Department. He served as Dean of the School of Computer Science from 2004 to 2014.

Dr. Bryant's research focuses on methods for formally verifying digital hardware, and more recently some forms of software. He is well known for the development of the ordered binary decision diagram (OBDD) data structure, used not just for formal hardware and software verification, but also digital circuit testing and synthesis, AI planning, and combinatorial optimization. In addition, he has developed several techniques to verify circuits by symbolic simulation, with levels of abstraction ranging from transistors to models based on first-order logic.

Dr. Bryant has received widespread recognition for his work. He is a fellow of the IEEE and the ACM, as well as a member of the National Academy of Engineering and the American Academy of Arts and Science. His awards include the 1997 ACM Kanellakis Theory and Practice Award (shared with Edmund M. Clarke, Ken McMillan, and Allen Emerson) for contributing to the development of symbolic model checking, as well as the 1989 IEEE W.R.G. Baker Prize for the best paper appearing in any IEEE publication during the preceding year. He received the 2010 ACM/IEEE A. Rihard Newton Technical Award in Electronic Design Automation, the 2009 EDAC/IEEE Phil Kaufman Award, and the 2007 IEEE Emmanuel R. Piore Award, reflecting the impact his work has had on tools used by the semiconductor industry for verifying their designs prior to manufacture.

Dr. Bryant teaches courses in computer systems. Along with David R. O'Hallaron, he 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,'' now in its third edition, is in use at over 320 universities worldwide, with translations into Chinese, Korean, Macedonian, and Russian.

Dr. Bryant spent the 1989-1990 academic year as a Visiting Research Fellow at Fujitsu Laboratories in Kawasaki, Japan, and the 2014-2015 academic year as Assistant Director for Information Technology Research and Development at the White House Office of Science and Technology Policy.


PhD, 1981 
Electrical Engineering and Computer Science 
Massachusetts Institute of Technology

EE, 1978 
Electrical Engineering 
Massachusetts Institute of Technology

SM, 1977 
Electrical Engineering 
Massachusetts Institute of Technology

BS, 1973 
Applied Mathematics 
University of Michigan, Ann Arbor


Professor Bryant's primary research interest is in formally verifying hardware designs. This interest grew out of earlier work in logic simulation and symbolic circuit analysis. Formal verification promises to eliminate the uncertainty that lingers even after extensive evaluation by techniques such as simulation.

During the course of developing hardware verification tools, he has become interested in symbolic representations and manipulation of discrete functions. The approach followed involves representing functions by directed acyclic graphs, known as Binary Decision Diagrams (BDDs). These methods are now being applied not just to circuit verification, but also to such areas as: temporal logic model checking, logic circuit optimization, automated theorem proving and truth maintenance systems.

Most recently, he has focused on the verification of superscalar microprocessors. In an effort to maximize the speed of program execution, modern processors apply techniques such as out-of-order execution, speculation and many forms of caching. Verifying that such a system faithfully preserves the sequential execution model of the instruction set architecture is both an intellectual and a logistical challenge. Recently developed techniques allow much of the data processing operations to be abstracted away, allowing the verifier to concentrate on control and communication. By exploiting properties of these abstract models, increasingly complex processors can be formally verified.