Randal E. Bryant

Education

1974–1981
Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, S.M. (1977), E.E. (1978), PhD (1981). Thesis Supervisor: Prof. Jack B. Dennis. MS Thesis Title: “Simulation of Packet Communication Architecture Computer Systems.” PhD Thesis Title: “A Switch-Level Simulation Model of Integrated Logic Circuits.”
1970–1973
University of Michigan, College of Engineering (Applied Math), B.S. (1973).

Employment

2020–present
Founders University Professor of Computer Science Emeritus, Carnegie Mellon University. Research areas: Boolean satisfiability, formal hardware and software verification.
2004–2020
University Professor of Computer Science, Carnegie Mellon University. Research areas: formal hardware and software verification, system testing, and computer science education. Teaching subjects: computer systems, distributed systems, parallel computing.
2014–2015
Assistant Director for Information Technology Research and Development, White House Office of Science and Technology Policy. Activities in: robotics, machine learning, high-performance computing, semiconductor technology, and cloud computing.
2004–2014
Dean, School of Computer Science, Carnegie Mellon University.
1999–2004
Head, Computer Science Department, Carnegie Mellon University.
1997–2004
Robert Mehrabian Professor of Computer Science, Carnegie Mellon University. Research areas: formal hardware and software verification, computer security. Teaching subjects: computer systems, computer networking, algorithms.
1992–1997
Professor of Computer Science, Carnegie Mellon University. Research areas: VLSI circuit verification, symbolic manipulation, and parallel computation. Teaching subjects: computer architecture
1987–1992
Associate Professor of Computer Science, Carnegie Mellon University. (Tenure granted Sept., 1990.) Research areas: VLSI simulation, VLSI circuit verification, symbolic manipulation, and parallel computation. Teaching subjects: introductory computer science, computer architecture, advanced VLSI design.
1990–1991
Visiting Research Fellow, Fujitsu Laboratories, Ltd., Kawasaki, Japan.
1984–1987
Assistant Professor of Computer Science, Carnegie Mellon University.
1984–present
Courtesy appointment in Electrical and Computer Engineering, Carnegie Mellon University.
1981–1984
Assistant Professor of Computer Science, California Institute of Technology. Research areas: VLSI circuit models, logic simulation, and circuit testing. Teaching subjects: computer architecture, digital systems theory, and computer algorithms.

Publication and Research Highlights

PIC
Google Scholar Citation Count. Downloaded 14-Feb-2024.

Most Cited Publications

  1. R. E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers, Vol. C-35, No. 8 (August, 1986), pp. 677–691.

    Foundational paper describing binary decision diagrams (BDDs) as data structure and algorithms for representing and manipulating Boolean functions in symbolic form. BDDs were described by Donald Knuth in a 2008 lecture as “one of the only really fundamental data structures that came out in the last twenty-five years.”

  2. R. E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams,” ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293–318.

    A tutorial and update on BDDs.

  3. K. S. Brace, R. L. Rudell, and R. E. Bryant, “Efficient Implementation of a BDD Package,” 27th Design Automation Conference, June, 1990, pp. 40–45.

    Describes a collection of refinements for implementing BDDs. Most BDD packages follow the implementation ideas described in this paper. At the 50th anniversary of the Design Automation Conference, this paper was listed as the one with the sixth highest citation count.

  4. M. Christodorescu, S. Jha, S. A. Seshia, D. Song, and R. E. Bryant, “Semantics Aware Malware Detection,” IEEE Symposium on Security and Privacy, May, 2005, pp. 32–46.

    Shows how to automatically remove the obfuscations generated by polymorphic malware programs to reveal the underlying code.

  5. R. E. Bryant, and D. R. O’Hallaron, Computer Systems: A Programmer’s Perspective, Prentice-Hall. First edition 2003, second edition 2011, third edition 2015.

    A textbook based on a course created at CMU that covers the combination of hardware, networking, and software that comprises a computer system. This book has been translated into Chinese, Russian, Korean, and Macedonian, and is in use at over 325 institutions worldwide.

  6. R. E. Bryant, “On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication,” IEEE Transactions on Computers, Vol. 40, No. 2 (February, 1991), pp. 205–213.

    Describes a method for proving that a particular class of Boolean functions will have exponentially-sized BDD representations. Showed that this case holds for the functions representing integer multiplication. This paper has been the subject of many refinements and extensions.

  7. R. E. Bryant, and Y.-A. Chen, “Verification of Arithmetic Circuits with Binary Moment Diagrams,” 32nd Design Automation Conference, June, 1995, pp. 535–541.

    Describes a variant on BDDs that can represent the word-level functionality of arithmetic circuits. Winner of best paper award in category “Verification, Simulation, and Test.” An early version of a general approach to verifying arithmetic circuits using polynomial representations.

  8. R. E. Bryant, “A Switch-Level Model and Simulator for MOS Digital Systems,” IEEE Transactions on Computers, (February, 1984), pp. 160–177.

    Describes the algorithmic basis for MOSSIM II, a logic simulator that models transistors as simple switches. This simulator and its successors were widely used in industry and academia in the 1980s. Intel used it to simulate several generations of microprocessor circuits.

  9. R. E. Bryant, Simulation of Packet Communication Architecture Computer Systems, Technical Report TR-188, MIT Laboratory for Computer Science, November, 1977.

    My masters thesis. Considered the first published work describing fully distributed, discrete-event simulation.

  10. C.-J. H. Seger, and R. E. Bryant, “Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories,” Formal Methods in System Design, Vol. 6, No. 2 (March, 1995), pp. 147–190.

    Describes symbolic trajectory evaluation, a method for formally verifying digital circuits via symbolic simulation. This approach was heavily used within Intel for many years.

  11. R. E. Bryant, R. H. Katz, and E. D. Lazowska, “Bit-data Computing: Creating Revolutionary Breakthroughs in Commerce, Science, and Society,” Computing Community Consortium, 2008.

    An early whitepaper proclaiming the potential benefits of large-scale, data-intensive computing.

Professional Activities

Affiliations

2018–2023
Chair, Data-Model Convergence Initiative Advisory Committee, Pacific Northwest National Laboratories.
2017–2023
Physical and Computational Sciences Directorate Advisory Committee, Pacific Northwest National Laboratories.
2016–2020
XSEDE Advisory Board (NSF-funded program for access to high performance computing resources.)
2015–2023
Alumni Advisory Board, University of Michigan Computer Science and Engineering Divison.
2011–2014
Infosys Prize jury member, Infosys Science Foundation.
2010
Review Committee for federal Networking and Information Technology Research and Development (NITRD) program on behalf of President’s Council of Advisors on Science and Technology (PCAST).
2010–2017
Council member, Computing Community Consortium
2010–present
American Academy of Arts and Sciences
2010–2014
Technical Advisory Board, Reveal Design Automation
2007–2014
Governing Board, Singapore Centre for Quantum Technology
2006–2012
Technical Advisory Board, NextOp Software (acquired by Atrenta, Inc.)
2006–2014
Academic Research Council, Singapore Ministry of Education.
2006–2009
Computer and Information Science and Engineering (CISE) Advisory Board, National Science Foundation.
2005–2011
Information Technology Advisory Board, Federal Bureau of Investigation.
2003–present
National Academy of Engineering. Section 5 (computer science and engineering) Peer Committee 2008–2009, Nominating Committee, 2010. Search committee executive 2010–2012. Vice Chair 2013–2014, Chair 2014–2015.
2003–2009
Technical Advisory Board, Nusym (acquired by Synopsys in 2010)
2000–2006
Board of Directors, Computing Research Assocation.
1999–2003
Technical Advisory Board, Innologic Systems (acquired by Synopsys in 2003).
1998–2000
Technical Advisory Board, Simplex Solutions (acquired by Cadence in 2002).
1993–2005
Technical Advisory Board, Fujitsu Labs of America, San Jose, CA.
1981–1985
Consultant: Hewlett Packard, Litton Data Systems, Digital Equipment Corporation, IBM, and other companies.
1978–present
ACM. Elected Fellow, 1999.
1977–present
IEEE. Elected Fellow, 1990.

Awards

2021
CAV Award. One of 21 recognized for “pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT).” Award given annually at the Computer Aided Verification Conference.
2013
Design Automation Conference. Recognized as coauthor of one of the 10 most cited papers, as one of the ten most cited authors, and for having published over 25 papers during the 50 year history of the conference.
2010
Elected to American Academy of Arts and Sciences.
2010
ACM/IEEE A. Richard Newton Technical Impact Award in Electronic Design Automation. Recognizing the impact of the 1986 paper “Graph-based algorithms for Boolean function manipulation.”
2009
Phil Kaufman Award, Electronic Design Automation Consortum (EDAC) and IEEE Council for Electronic Design Automation. Citation: “for his seminal breakthroughs in the area of formal verification.”
2008
University of Michigan Distinguished Engineering Alumni Award.
2007
IEEE Emanuel R. Piore Award. Citation: “For seminal contributions to the field of computer-aided circuit design and verification, including the development and promulgation of ordered binary decision diagrams.”
2003
IEEE CAD Transactions Best Paper Award. For paper coauthored with Ph.D. student Yirng-An Chen.
2003
Elected to National Academy of Engineering. Citation: “For contributions to symbolic simulation and logic verification.”
2003
Paper selected for inclusion in The Best of ICCAD, 20 Years of Excellence in Computer-Aided Design, a collection of 42 out of over 2,200 papers that have been presented at the International Conference on Computer-Aided Design between 1983 and 2002.
2000
Golden Jubilee Medal. Awarded to 118 members of the IEEE Circuits and Systems Society for professional contributions.
1999
Elected Fellow, ACM.
1998
Allen Newell Research Excellence Medal, Computer Science Department, Carnegie Mellon University.
1998
ACM Kanellakis Theory and Practice Award. Shared with Ken McMillan, Edmund M. Clarke, and Allen Emerson for the development of symbolic model checking
1996
Technical Excellence Award, Semiconductor Research Corporation. Shared with Ken McMillan and Edmund M. Clarke for the development of symbolic model checking.
1995
Litton Fellow, Carnegie Mellon Computer Science Department.
1995
Best Paper Award, Simulation, Verification, and Test Category, 32nd Design Automation Conference, for paper coauthored with Ph.D. student Yirng-An Chen.
1990
Elected Fellow, IEEE. Citation: “for contributions to switch-level simulation of very large scale integrated circuits.”
1990
Inventor Recognition Award, Semiconductor Research Corporation, for the BDD symbolic Boolean manipulation software library.
1989
Inventor Recognition Award, Semiconductor Research Corporation. for the COSMOS switch-level simulator.
1989
IEEE W. R. G. Baker Award for “The most outstanding paper reporting original work in any of the IEEE Transactions, Proceedings of the IEEE, journals, or magazines issued during the previous year.”
1988
Best Paper Award, Design, Simulation and Test Category, 25th Design Automation Conference. For paper coauthored with Ph.D. student Derek Beatty.
1988
Two papers selected for inclusion in Twenty Five Years of Electronic Design Automation, a collection of 77 of the over 1600 papers presented at the Design Automation Conferences for the years 1964–1987.
1987
IEEE CAD Transactions Best Paper Award.
1983, 1984
IBM Faculty Development Award (One of 100 recipients of special grant for junior faculty.)
1974–1978
National Science Foundation Graduate Fellow.

Academic Review Committees

2022
University of California, Santa Barbara, Computer Science Department.
2017
Stanford University, Computer Science Department.
2015
Iowa State University, Electrical and Computer Engineering Department.
2012
University of Michigan, Computer Science and Engineering Division.
2011
University of California, San Francisco, Bioinformatics Advisory Panel.
2010
Washington University St. Louis, School of Engineering and Applied Science.
2009
University of Tokyo, Graduate School of Information Science and Technology.
2009
University of Utah, School of Computing.
2009
Princeton University, Computer Science Department.
2009
University of Virginia, Computer Science Department.
2009–2013
Massachusetts Institute of Technology, Department of EECS.
2009
University of Washington, Computer Science Department.
2007
Georgia Institute of Technology, College of Computing.
2007
Stanford University, Computer Science Department.
2005
University of Virginia, Computer Science Department.
2004
Kuwait University, Graduate program in computer science.
2004
Information Technology University of Copenhagen, Denmark.
2003
University of Pittsburgh, Computer Science Department.
2003
University of Utah, School of Computing.
2002
University of Texas, Computer Science Department.
2001
Stanford University, Electrical Engineering Department.
2000
Technion, Haifa, Israel, Faculty of Computer Science.

Conference Committees

2018
Organizing Committee, NITRD Big Data and High End Computing Interagency Working Groups Joint Workshop.
2015
Co-organizer, White House Workshop on the National Strategic Computing Initiative
2011, 2012
Program Committee, International Conference on Theory and Applications of Satisfiability Testing.
2008
Co-organizer, Hadoop Summit and Symposium on Data-Intensive Computing, Sunnyvale, CA.
2002–2004
Program Committee, Design and Test in Europe.
1996, 1998, 2000, 2002, 2004
Program Committee, International Conference on Formal Methods in Computer-Aided Design.
1990, 1994, 2000–2001, 2004, 2006
Program Committee, International Conference on Computer-Aided Verification.
1994–2000
Executive Committee, Design Automation Conference (tutorial chair 1994–1995, program co-chair 1998–1999).
1990, 1992
Program Committee, TAU International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems.
1991, 1993
Program Committee, International Workshop on Logic Synthesis.
1989
Program Committee, IFIP Workshop on Applied Formal Methods for Correct VLSI Design.
1986–1992
Program Committee, Design Automation Conference.
1989–1990
Program Committee, Microelectronic System Education Conference.
1989
Program Committee, International Conference on Compuer-Aided Design.
1988
Program Committee, IFIP Conference on Design Methodologies for VLSI and Computer Architecture.
1987
Program Committee, IEEE VLSI Workshop, Clearwater Beach, Florida.
1985–1991, 1997
Program Committee, Conference on Advanced Research in VLSI (held at MIT, Caltech, UNC, Brown, and Michigan).
1983
Chairman, Third Caltech Conference on Very Large Scale Integration.
1979
Organizer, MIT Workshop on Self-Timed Systems.

Review Committees

2019
NSF CISE Committee of Visitors
2001
Texas Advanced Research/Advanced Technology Programs Reviewer.
2001
National Science Foundation CAREER Program Proposal Panel.
2001
National Science Foundation ITR Program Preproposal Panel.
1990
National Science Foundation Graduate Fellowship evaluation panel.

Editorships and Reviewing

1995–1997
Editor-in-Chief, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems.
1991–2000
Editorial Board, Formal Methods in System Design
1989–1995
Associate Editor, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems.
1976–present
Reviewer for papers submitted to IEEE Transactions on Computers, IEEE Computer, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on Software Engineering, IEEE Transactions on Circuits and Systems, ACM Transactions on Computing Systems, Journal of the ACM, International Journal of Parallel Programming, Communications of the ACM, Theoretical Computer Science, Information Processing Letters, and numerous conferences.
1983–1988
Reviewer for ACM Distinguished Dissertation Award

University Service

2020–2021
Academic Freedom Commission, reviewing CMU’s policies on academic freedom and freedom of expression
2020–2021
Faculty Senate Chair Emeritus.
2019–2020
Faculty Senate Chair.
2019–2020
Member of review committee for Dean of Dietrich College of Humanities and Social Science.
2017–2019
Faculty Senate Vice Chair.
2017
Chair of search committee for Dean of Carnegie Mellon University, Qatar.
2015–2016
Member of review committee for Dean of Carnegie Mellon University, Qatar.
2007
Member of Search Committee for Dean of Mellon College of Science
2004
Member of Search Committee for Director of Robotics Institute.
2000
Member of Provost Search Committee
1998–1999
Co-Chair of School of Computer Science Dean Search Committee
1993–1999
In charge of faculty reappointments and promotions, Computer Science Department.
1991–1993
School of Computer Science Graduate Council. Chairman-Elect 1991–1992, Chairman 1992–1993.
1991–1993
Member, CMU Faculty Development Awards Committee
1992
Member of School of Computer Science Dean Search Committee
1988–1989
Presidential appointee to CMU Faculty Senate.
1988–1990
Graduate Admissions Committee, CMU Computer Science (Chairman, 1989).
1985–1987
Qualifier Review Committee, CMU Computer Science Dept. (Chairman, 1986–1987).
1986–1987
University Research Council, CMU.
1986–1988
Facilities Advisory Committee, CMU Computer Science Dept.
1981-1984
Organized Computer Science Seminar series, Caltech.
1982-1984
In charge of Computer Science Library, Caltech.
1982
Computer Science Graduate Admissions Committee, Caltech.

Community Service

2020–present
Board of Directors, Bach Choir of Pittsburgh
2015–present
Member of Bass Section, Bach Choir of Pittsburgh
2011–2014
Member of Bass Section, Pittsburgh Gospel Choir
2001–2014
Board of Directors, Steel City Rowing Club, Pittsburgh, PA. Board president 2005–2014.
1998–2000, 2003–2006, 2017–2023
Board of Session, Bellefield Presbyterian Church, Pittsburgh, PA.
1986–1990
Board of Trustees, Bellefield Presbyterian Church, Pittsburgh, PA.