Randal E Bryant

Timeline

1. 1973–1984

   A doctorate and MOSSIM

   He earns a bachelor's degree in applied mathematics at the University of Michigan in 1973 and a doctorate in electrical engineering and computer science at MIT in 1981, then works as an assistant professor of computer science at Caltech until 1984. His MOSSIM switch-level simulator, developed in 1983, is the first tool to model very large-scale integrated circuits accurately, and Intel uses it for more than a decade.

2. 1984–1986

   Binary decision diagrams at CMU

   He joins Carnegie Mellon in 1984 and develops efficient algorithms based on binary decision diagrams (BDDs) in 1985. His 1986 paper "Graph-Based Algorithms for Boolean Function Manipulation" presents BDDs as a data structure for Boolean functions, and it reaches the highest citation count of any publication in the Citeseer database. BDDs go on to serve circuit verification, synthesis and testing as well as artificial intelligence planning and compiler optimization.

3. 1998–2009

   Awards for circuit verification

   He shares the 1998 ACM Paris Kanellakis Theory and Practice Award with Edmund Clarke, E. Allen Emerson and Kenneth McMillan for their invention of symbolic model checking. The National Academy of Engineering elects him in 2003, the IEEE gives him its Emanuel R. Piore Award in 2007, and the EDAC/IEEE Phil Kaufman Award follows in 2009 for breakthroughs in formal verification.

4. 2004–2014

   Dean of computer science

   He serves as dean of Carnegie Mellon's School of Computer Science from 2004 to 2014 and is reappointed in 2009. During his tenure the school builds a big data emphasis, establishes the world's first Machine Learning Department, and sees annual research funding more than double to $99 million.

5. By 2014

   A computer systems textbook

   With David O'Hallaron, he creates Carnegie Mellon's computer systems course 15-213 and writes the textbook "Computer Systems: A Programmer's Perspective" from it. The book is in use at over 240 institutions worldwide by 2014.

6. 2014–2015

   Big data at the White House

   In August 2014, he starts a sabbatical assignment as assistant director for information technology research and development at the White House Office of Science and Technology Policy, advising on big data. His work there covers robotics, machine learning, high-performance computing and the National Strategic Computing Initiative. From 2006 to 2017, he also serves on the council of the Computing Community Consortium.

7. 2015–2020

   Parallel computing and retirement

   Back from Washington, he teaches parallel computing at Carnegie Mellon, a subject he had taken up at OSTP. He retires in June 2020 and becomes Founders University Professor of Computer Science, Emeritus.

8. As of October 2026

   Verified model counting research

   He is Founders University Professor of Computer Science, Emeritus at Carnegie Mellon, with a courtesy appointment in Electrical and Computer Engineering. In 2025, he coauthors the first formally verified toolchain for weighted and unweighted model counting with Wojciech Nawrocki, Jeremy Avigad and Marijn Heule, and writes a paper on weighted model counting, which finds uses in probabilistic reasoning. In July 2026, he coauthors "Factoring Learned Clauses", a SAT 2026 conference paper with Armin Biere, Marijn Heule and others.