Randal E. Bryant

- 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.
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).

- 2014-present
- 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-present
- 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.
- 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.

Google Scholar Citation Count. Downloaded 03-Aug-2015.

- 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.''

- 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.

- 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.

- 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.

- 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.

- 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.''

- 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 was widely used in industry and academia in the 1980s. Intel used it to simulate several generations of microprocessor circuits.

- 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.

- 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 250 institutions worldwide.

- 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 is heavily used within Intel.

- 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-2014
- Council member, Computing Community Consortium.
- 2010-present
- American Academy of Arts and Sciences.
- 2010-present
- Technical Advisory Board, Reveal Design Automation
- 2006-2012
- Technical Advisory Board, NextOp Software (acquired by Atrenta, Inc.)
- 2007-2014
- Governing Board, Singapore Centre for Quantum Technology
- 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.
- 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-present
- 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.

- 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.

- 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, Department of Computer Science.
- 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
- Faculty of Computer Science, Technion, Haifa, Israel.

- 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.

- 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.

- 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

- 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 of Computer Science Graduate Council.
Chairman-Elect 1991-1992, Chairman 1992-1993.
- 1991-1993
- Member, CMU Faculty Development Awards Committee
- 1992
- 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.

R. E. Bryant, and D. R. O'Hallaron,
*Computer Systems: A Programmer's Perspective, Second Edition*,
Prentice-Hall, 2011.
More information available at
`http://csapp.cs.cmu.edu/`.

R. E. Bryant, and J. H. Kukula,
``Formal Methods for Functional Verification,''
in *The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design*,
A. Kuehlmann, *ed.*
Kluwer Academic Publishers, 2003,
pp. 3-16.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccad-best02.pdf`.

R. E. Bryant, and D. R. O'Hallaron,
*Computer Systems: A Programmer's Perspective*,
Prentice-Hall, 2003.

R. E. Bryant, and C. Meinel,
``Ordered Binary Decision Diagrams,''
in *Logic Synthesis and Verification*,
S. Hassoun and T. Sasao, *eds.*,
Kluwer Academic Publishers, 2001.

R. E. Bryant,
``Data-Intensive Scalable Computing for Scientific Applications,''
*IEEE Computing in Science and Engineering*,
Vol. 13, No. 6 (2011),
pp. 25-33.

R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman,
and B. Brady,
``An Abstraction-Based Decision Procedure for Bit-Vector Arithmetic,''
*International Journal of Software Tools for Technology*,
Springer-Verlag
Vol. 11, No. 2 (April, 2009),
pp. 95-104.

R. M. Jensen, M. M. Veloso, and R. E. Bryant,
``State-Set Branching: Leveraging BDDs for Heuristic Search,''
*Artificial Intelligence*,
Vol. 172, Issues 2-3 (February, 2008),
pp. 103-139.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/aij07.pdf`.

S. K. Lahiri, and R. E. Bryant,
``Predicate Abstraction with Indexed Predicates,''
*ACM Transactions on Computational Logic*,
Vol. 9, No. 1 (Dec., 2007).
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tocl06.pdf`.

S. A. Seshia, K. Subramani, and R. E. Bryant,
``On Solving Boolean Combinations of UTVPI Constraints,''
*Journal of Satisfiability, Boolean Modeling and Computation*,
Vol. 3 (2007), pp. 67-90.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/jsat07.pdf`.

M. N. Velev, and R. E. Bryant,
``TLSim and EVC: A Term-Level Symbolic
Simulator and an Efficient Decision Procedure for the Logic of
Equality with Uninterpreted Functions and Memories,''
*International Journal of Embedded Systems*,
Vol. 1, No. 1/2 (2005), pp. 134-149.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/ijes05.pdf`.

S. A. Seshia, and R. E. Bryant, ``Deciding Quantifier-Free Presburger
Formulas Using Parameterized Solution Bounds,''
*Logical Methods in Computer Science*,
Vol. 1, Issue 2, Paper 7 (December, 2005).
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/lmcs05.pdf`.

M. N. Velev, and R. E. Bryant, ``Effective Use of Boolean
Satisfiability Procedures in the Formal Verification of Superscalar
and VLIW Microprocessors,'' *Journal of Symbolic Computation*.
Vol. 35, No. 2 (February, 2003), pp. 73-106. Submitted version available as
`http://www.cs.cmu.edu/~bryant/pubdir/jsc03.pdf`.

R. E. Bryant and M. N. Velev, ``Boolean Satisfiability with Transitivity
Constraints,''
*ACM Transactions on Computational Logic*,
Vol. 3, No. 4 (October, 2002).
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tocl-trans01.pdf`.

Y.-A. Chen, and R. E. Bryant, ``An Efficient Graph Representation for
Arithmetic Circuit Verification,'' *IEEE Transactions on
Computer-Aided Design of Integrated Circuits and Systems*, Vol. 20,
No. 12 (December, 2001), pp. 1442-1454. Winner of 2003 IEEE CAD
Transactions Best Paper Award.
Preprint version available as
`http://www.cs.cmu.edu/~bryant/pubdir/tcad01-chen.pdf`.

R. E. Bryant, and Y.-A. Chen,
``Verification of Arithmetic Circuits Using Binary Moment Diagrams,''
*Software Tools for Technology Transfer*, Springer-Verlag,
Vol. 3, No. 2 (May, 2001), pp. 137-155.
Submitted version available as
`http://www.cs.cmu.edu/~bryant/pubdir/sttt-submit.pdf`.

C. B. McDonald and R. E. Bryant,
``CMOS Circuit Verification with Symbolic Switch-Level Timing Simulation,''
*IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems*,
Vol. 20, No. 3 (March
, 2001), pp. 458-474.
Preprint version available as
`http://www.cs.cmu.edu/~bryant/pubdir/tcad01.pdf`.

R. E. Bryant, S. German, M. N. Velev, ``Processor Verification Using
Efficient Reductions of the Logic of Uninterpreted Functions to
Propositional Logic,''
*ACM Transactions on Computational Logic*,
Vol. 2, No. 1 (January, 2001).
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tocl01.pdf`.

M. Pandey, and R. E. Bryant,
``Exploiting symmetry when verifying transistor-level circuits by
symbolic trajectory evaluation,''
*IEEE Transactions on Computer-Aided Design of Integrated Circuits
and Systems*,
Vol. 18, No. 7 (July, 1999), pp. 918-935.
Winner of 2001 IEEE Circuits and Systems Society Outstanding Young
Author Award.
Preprint version available as
`http://www.cs.cmu.edu/~bryant/pubdir/tcad99.pdf`.

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.
Preprint version available as
`http://www.cs.cmu.edu/~bryant/pubdir/fmsd95.pdf`.

R. E. Bryant, J. D. Tygar, and L. P. Huang,
``Geometric Characterization of Series-Parallel Variable Resistor
Networks,''
*IEEE Transactions on Circuits and Systems I:
Fundamental Theory and Applications*, Vol. 41, No. 11 (November, 1994),
pp. 686-698.
Manuscript version available as
`http://www.cs.cmu.edu/~bryant/pubdir/tcas94.pdf`.

R. E. Bryant,
``Symbolic Boolean Manipulation with Ordered Binary Decision
Diagrams,''
*ACM Computing Surveys*,
Vol. 24, No. 3 (September, 1992), pp. 293-318.
Preprint version published as CMU Technical Report CMU-CS-92-160,
`http://www.cs.cmu.edu/~bryant/pubdir/CMU-CS-92-160.pdf`. Also available as
`http://www.cs.cmu.edu/~bryant/pubdir/acmcs92.pdf`

R. E. Bryant,
``A Methodology for Hardware Verification Based on Logic Simulation,''
*J.ACM*, Vol. 38, No. 2 (April, 1991), pp. 299-328.
Preprint available as
`http://www.cs.cmu.edu/~bryant/pubdir/jacm91.pdf`.

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.
Preprint available as
`http://www.cs.cmu.edu/~bryant/pubdir/ieeetc91.pdf`.

R. E. Bryant,
``Formal Verification of Memory Circuits by Switch-Level Simulation,''
*IEEE Transactions on Computer-Aided Design
of Integrated Circuits and Systems*, Vol. 10, No. 1 (January, 1991),
pp. 94-102. Preprint available as
`http://www.cs.cmu.edu/~bryant/pubdir/tcad91.pdf`.

R. E. Bryant,
``Algorithmic Aspects of Symbolic Switch Network Analysis,''
*IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems*,
Vol. CAD-6, No. 4 (July, 1987), pp. 618-633. Winner of 1987 IEEE CAD
Transactions Best Paper Award, and the 1989 IEEE W. R. G. Baker Award.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tcad87a.pdf`.

R. E. Bryant,
``Boolean Analysis of MOS Circuits,''
*IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems*,
Vol. CAD-6, No. 4 (July, 1987), pp. 634-649. Winner of the IEEE W. R. G.
Baker Award.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tcad87b.pdf`.

R. E. Bryant,
``Graph-Based Algorithms for Boolean Function Manipulation,''
*IEEE Transactions on Computers*, Vol. C-35, No. 8 (August, 1986),
pp. 677-691.
Reprinted in
M. Yoeli,
*Formal Verification of Hardware Design*,
IEEE Computer Society Press, 1990, pp. 253-267.
Electronic version with annotations available as
`http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf`.

R. E. Bryant,
``A Switch-Level Model and Simulator for MOS Digital Systems,''
*IEEE Transactions on Computers*,
Vol. C-33, No. 2
(February, 1984), pp. 160-177.

H. Cui, J. Simsa, Y.-H. Ling, H. Li, B. Blum, X. Xu, J. Yang,
G. A. Gibson, and R. E. Bryant, ``PARROT: A Practical Runtime for
Deterministic, Stable, and Reliable Threads,'' *24th ACM Symposium
on Operating Systems Principles*, 2013.

J. Simsa, R. Bryant, G. A. Gibson, and J. Hickey,
``Scalable Dynamic Partial Order Reduction,''
*3rd International Conference on Runtime Verification*, 2012.

B. A. Brady, R. E. Bryant, and S. A. Seshia,
``Learning Conditional Abstractions,''
*Formal Methods in Computer-Aided Design*,
October, 2011,
pp. 116-124.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/fmcad11.pdf`

J. Simsa, G. A. Gibson, and R. E. Bryant,
``dBug: Systematic Testing of Unmodified Distributed and Multi-Threaded Programs,''
*18th International Workshop on Model Checking of Softare (SPIN '11)*,
2011.

B. A. Brady, R. E. Bryant, S. A. Seshia, and J. W. O'Leary,
``ATLAS: Automatic Term-Level Abstraction of RTL Designs,''
*Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)*,
July, 2010.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/memocode10.pdf`.

R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman,
and B. Brady,
``Deciding Bit-Vector Arithmetic with Abstraction,''
*Tools and Algorithms for the
Construction and Analysis of Systems TACAS 2007*,
April, 2007.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tacas07.pdf`.

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.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/oakland05.pdf`.

V. Ganapathy, S. A. Seshia, S. Jha, T. W. Reps, and R. E. Bryant,
``Automatic Discovery of API-Level Exploits,''
*International Conference on Software Engineering ICSE 05*,
May, 2005,
pp. 312-321.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/icse05.pdf`.

S. A. Seshia, R. E. Bryant, and K. S. Stevens,
``Modeling and Verifying Circuits Using Generalized Relative Timing,''
*IEEE International Symposium on Asynchronous Circuits and Systems, ASYNC 05*,
March, 2005,
pp. 98-108
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/async05.pdf`.

S. K. Lahiri and R. E. Bryant,
``Indexed Predicate Discovery for Unbounded System Verification,''
*Computer-Aided Verification CAV 2004*,
R. Alur, and D. A. Peled, *eds*.,
LNCS 3114, Springer-Verlag,
July, 2004,
pp. 135-147.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav04b.pdf`.

A. Goel and R. E. Bryant,
``Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Function Vectors,''
*Computer-Aided Verification CAV 2004*,
R. Alur, and D. A. Peled, *eds*.,
LNCS 3114, Springer-Verlag,
July, 2004,
pp. 255-267.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav04a.pdf`.

S. A. Seshia and R. E. Bryant,
``Deciding Quantifier-Free Presburger Formulas Using
Parameterized Solution Bounds,''
*Logic in Computer Science LICS 2004*, IEEE,
July, 2004,
pp. 100-109.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/lics04.pdf`.

R. M. Jensen, M. M. Veloso, and R. E. Bryant,
``Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic Non-Deterministic Planning,''
*International Conference on Automated Planning and Scheduling ICAPS 04*,
June, 2004.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/icaps04.pdf`.

S. K. Lahiri, R. E. Bryant, A. Goel, and M. Talupur
``Revisiting Positive Equality,''
*Tools and Algorithms for the
Construction and Analysis of Systems TACAS 2004*,
K. Jensen, and A. Podelski, *eds*.,
LNCS 2988, Springer-Verlag,
March, 2004,
pp. 1-15
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tacas04.pdf`.

S. K. Lahiri, and R. E. Bryant,
``Constructing Quantified Invariants via Predicate Abstraction,''
*Verification, Model Checking, and Abstract Interpretation (VMCAI '04)*,
B. Steffen, and G. Levi, *eds*.,
LNCS 2937, Springer-Verlag,
February, 2004,
pp. 267-281.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/vmcai04.pdf`. Slightly longer version available (as gzipped postscript) as
`http://www.cs.cmu.edu/~bryant/pubdir/vmcai04-long.ps.gz.pdf`

R. E. Bryant, S. K. Lahiri, and S. A. Seshia,
``Convergence Testing in Term-Level Bounded Model Checking,''
*Correct Hardware Design and Verification Methods CHARME '03*.
D. Geist, and E. Tronci, *eds.*, LNCS 2860,
Springer-Verlag, October, 2003, pp. 348-362.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/charme03.pdf`.

R. M. Jensen, M. M. Veloso, and R. E. Bryant,
``Guided Symbolic Universal Planning,''
*International Conference on Automated Planning and Scheduling ICAPS 03*,
pp. 123-132,
2003.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/icaps03.pdf`

S. K. Lahiri, and R. E. Bryant,
``Deductive Verification of Advanced Out-of-Order Microprocessors,''
*Computer-Aided Verification CAV '2003*,
W. A. Hunt, Jr., and F. Somenzi, *eds.*, LNCS 2725,
Springer-Verlag, July, 2003, pp. 341-354.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav03a.pdf`

S. K. Lahiri, R. E. Bryant, and B. Cook,
``A Symbolic Approach to Predicate Abstraction,''
*Computer-Aided Verification CAV '2003*,
W. A. Hunt, Jr., and F. Somenzi, *eds.*, LNCS 2725,
Springer-Verlag, July, 2003, pp. 141-153.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav03b.pdf`

S. A. Seshia, and R. E. Bryant,
``Unbounded, Fully Symbolic Model Checking of Timed Automata
using Boolean Methods,''
*Computer-Aided Verification CAV 2003*,
W. A. Hunt, Jr., and F. Somenzi, *eds.*, LNCS 2725,
Springer-Verlag, July, 2003, pp. 154-166.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav03c.pdf`

S. A. Seshia, S. K. Lahiri, and R. E. Bryant,
``A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions,''
*40th Design Automation Conference*,
2003, pp. 425-430.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac03a.pdf`

A. Goel, G. Hasteer, and R. E. Bryant,
``Symbolic Representation with Ordered Function Templates,''
*40th Design Automation Conference*,
2003, pp. 431-435.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac03b.pdf`

A. Goel, and R. E. Bryant
``Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis,''
*Design and Test Europe DATE 2003*,
March, 2003.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/date03.pdf`.

S. K. Lahiri, S. A. Seshia, and R. E. Bryant,
``Modeling and Verification of Out-of-Order Processors in UCLID,''
*Formal Methods in Computer-Aided Design FMCAD '2002*,
M. D. Aagaard and J. W. O'Leary, *eds.*, LNCS 2517,
November, 2002, pp. 142-159. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/fmcad02.pdf`.

R. E. Bryant, S. K. Lahiri, and S. A. Seshia,
``Modeling and Verifying Systems using a Logic of Counter Arithmetic
with Lambda Expressions and Uninterpreted Functions,''
*Computer-Aided Verification CAV '2002*,
E. Brinksma, and K. G. Larsen, *eds.*,
LNCS 2404,
Springer-Verlag, July, 2002, pp. 78-92.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav02a.pdf`

O. Strichtman, S. A. Seshia, and R. E. Bryant,
``Deciding Separation Formulas with SAT,''
*Computer-Aided Verification CAV '2002*,
E. Brinksma, and K. G. Larsen, *eds.*,
LNCS 2404,
Springer-Verlag, July, 2002, pp. 209-222.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav02b.pdf`

R. M. Jensen, R. E. Bryant, and M. M. Veloso,
``An Efficient BDD-Based A* Algorithm,''
*Proceedings of AIPS-02 Workshop on Planning via Model Checking*,
2002.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/aips02.pdf`

R. M. Jensen, R. E. Bryant, and M. M. Veloso,
``SetA*: An Efficient BDD-Based Heuristic Search Algorithm,''
*Proceedings of the 18th National Conference on Artificial Intelligence
AAAI-02*,
2002.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/aaai02.pdf`

M. N. Velev, and R. E. Bryant,
``EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations,''
*Computer-Aided Verification CAV '2001*,
G. Berry, H. Comon, and A. Finkel, *eds.*, LNCS 2102,
Springer-Verlag, July, 2001, pp. 235-240.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav01.pdf`

C. B. McDonald, and R. E. Bryant,
``Computing Logic-Stage Delays Using Circuit Simulation and Symbolic
Elmore Analysis,''
*38th Design Automation Conference DAC 2001*,
June, 2001. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac01a.pdf`

M. N. Velev, and R. E. Bryant,
``Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors,''
*38th Design Automation Conference DAC 2001*,
June, 2001. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac01b.pdf`

R. E. Bryant, and D. R. O'Hallaron,
``Teaching Computer Systems from a Programmer's Perspective,''
*32nd Technical Symposium on Computer Science Education SIGCSE '01*,
February, 2001.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/sigcse01.pdf`.

R. E. Bryant, P. Chauhan, E. M. Clarke, and A. Goel,
``A Theory of Consistency for Modular Synchronous Systems,''
*Formal Methods in Computer-Aided Design FMCAD '2000*,
W. A. Hunt, Jr., and S. D. Johnson, *eds.*, LNCS 1954,
November, 2000. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/fmcad00a.pdf`.

C. Wilson, D. L. Dill, and R. E. Bryant,
``Symbolic Simulation with Approximate Values,''
*Formal Methods in Computer-Aided Design FMCAD '2000*,
W. A. Hunt, Jr., and S. D. Johnson, *eds.*, LNCS 1954,
November, 2000,
pp. 486-504. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/fmcad00b.pdf`.

R. E. Bryant, and M. N. Velev,
``Boolean Satisfiability with Transitivity Constraints,''
*Computer-Aided Verification CAV '2000*,
E. A. Emerson and A. P. Sistla, *eds.*, LNCS 1855,
Springer-Verlag, July, 2000, pp. 85-98,
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav00.pdf`.

C. B. McDonald, and R. E. Bryant,
``Symbolic Timing Simulation Using Cluster Scheduling,''
*37th Design Automation Conference DAC 2000*,
pp. 254-259,
June, 2000. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac00a.pdf`

M. N. Velev, and R. E. Bryant,
``Formal Verification of Superscalar
Microprocessors with Multicycle Functional Units, Exceptions, and
Branch Predication,''
*37th Design Automation Conference DAC 2000*,
pp. 112-117,
June, 2000. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac00b.pdf`

C. B. McDonald, and R. E. Bryant,
``Symbolic Functional and Timing Verification of Transistor-Level Circuits,''
*International Conference on Computer-Aided Design (ICCAD '99)*,
November, 1999.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccad99.pdf`.

M. N. Velev, and R. E. Bryant,
``Superscalar Processor Verification Using Efficient Reductions of the
Logic of Equality with Uninterpreted Functions,''
*Correct Hardware Design and Verification Methods CHARME '99*,
L. Pierre, and T. Kropf, *eds.*, LNCS 1703,
Springer-Verlag,
September, 1999, pp. 37-53.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/charme99.pdf`.

R. E. Bryant, S. German, and M. N. Velev,
``Exploiting Positive Equality in a Logic of Equality
With Uninterpreted Functions,''
*Computer-Aided Verification CAV '99*,
N. Halbwachs, and D. Peled, *eds.*, LNCS 1633,
Springer-Verlag,
July, 1999, pp. 470-482.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav99a.pdf`.

B. Yang, R. Simmons, R. E. Bryant, and D. R. O'Hallaron,
``Optimizing Symbolic Model Checking for Constraint-Rich Models,''
*Computer-Aided Verification CAV '99*, 1999.
N. Halbwachs, and D. Peled *eds.*, LNCS 1633,
Springer-Verlag,
July, 1999, pp. 328-340.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav99b.pdf`. Expanded version available as
Technical Report
`http://reports-archive.adm.cs.cmu.edu/anon/1999/CMU-CS-99-118.ps`.

V. A. Patankar, A. Jain, and R. E. Bryant,
``Formal Verification of an ARM Processor,''
*12th International Conference on VLSI Design*,
Goa, India, Jan. 1999.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/vlsi99.vishnu.pdf`

M. N. Velev, and R. E. Bryant,
``Exploiting Positive Equality and Partial Nonconsistency in the Formal
Verification of Pipelined Microprocessors,''
*36th Design Automation Conference DAC '99*, June, 1999,
pp. 397-401.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac99.pdf`

M. N. Velev, and R. E. Bryant,
``Bit-level
abstraction in the verification of pipelined microprocessors by
correspondence checking.''
*Formal Methods in Computer-Aided Design FMCAD '98*,
G. Gopalakrishnan and P. Windley, *eds.*, LNCS 1522, Springer-Verlag,
November, 1998, pp. 18-35.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/fmcad98a.pdf`.

B. Yang, R. E. Bryant, D. R. O'Hallaron, A. Biere, O. Coudert,
G. Janssen, R. K. Ranjan, and F. Somenzi,
``A Performance Study of BDD-Based Model Checking,''
*Formal Methods in Computer-Aided Design FMCAD '98*,
G. Gopalakrishnan and P. Windley, *eds.*, LNCS 1522, Springer-Verlag,
November, 1998, pp. 255-289.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/fmcad98b.pdf`.

M. N. Velev, and R. E. Bryant,
``Incorporating Timing Constraints in
the Efficient Memory Model for Symbolic Ternary Simulation,''
*International Conference on Computer Design ICCD '98*,
IEEE,
October, 1998, pp. 400-406.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccd98.pdf`.

Y.-A. Chen, and R. E. Bryant,
``Verification of Floating Point Adders,''
*Computer-Aided Verification CAV '98*,
A. J. Hu and M. Y. Vardi, *eds.*, LNCS 1427, Springer-Verlag,
June, 1998, pp. 488-499.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav98.pdf`

B. Yang, Y.-A. Chen, R. E. Bryant, and D. R. O'Hallaron,
``Space- and Time-Efficient BDD Construction by Working Set Control,''
*Asian-Pacific Design Automation Conference ASPDAC '98*,
Feb., 1998, pp. 423-432.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/aspdac98.pdf`.

M. N. Velev, and R. E. Bryant,
``Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation,''
*International Conference on Tools and Algorithms for the
Construction and Analysis of Systems TACAS '98*,
B. Steffen, *ed.*,
LNCS 1384,
Springer-Verlag, March 1998, pp. 136-150.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tacas98.pdf`.

M. N. Velev, and R. E. Bryant, ``Verification of Pipelined
Microprocessors by Correspondence Checking in Symbolic Ternary
Simulation,'' *International Conference on Application of
Concurrency to System Design CSD '98*, IEEE, March, 1998.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/csd98.pdf`.

M. N. Velev, and R. E. Bryant,
``Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation,''
*Asian Computer Science Conference ASIAN '97*,
R. K. Shyamasundar and K. Ueda, *eds.*,
LNCS 1345,
Springer-Verlag, December 1997, pp. 18-31.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/asian97.pdf`.

Y.-A. Chen, and R. E. Bryant,
``*PHDD: An Efficient Graph Representation for Floating Point Circuit Verification,''
*International Conference on Computer-Aided Design ICCAD '97*,
November, 1997, pp. 2-7.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccad97.pdf`.

M. Pandey, and R. E. Bryant,
``Formal Verification of Memory Arrays using Symbolic Trajectory Evaluation,''
*IEEE International Workshop on Memory Technology, Design and Testing*,
August, 1997.

M. Pandey, and R. E. Bryant,
``Exploiting Symmetry when Verifying Transistor-Level Circuits by Symbolic Trajectory Evaluation,''
*Computer-Aided Verification CAV '97*,
O. Grumberg, *ed.*,
LNCS 1254,
Springer-Verlag, June, 1997, pp. 244-255.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav97a.pdf`.

M. N. Velev, R. E. Bryant, and A. Jain,
``Efficient Modeling of Memory Arrays in Symbolic Simulation,''
*Computer-Aided Verification CAV '97*,
O. Grumberg, *ed.*,
LNCS 1254,
Springer-Verlag, June, 1997, pp. 388-399.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cav97b.pdf`.

K. L. Nelson, A. Jain, and R. E. Bryant,
``Formal Verification of a Superscalar Execution Unit,''
*34th Design Automation Conference DAC '97*, June, 1997,
pp. 161-166.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac97a.pdf`

M. Pandey, R. E. Bryant, R. Raimi, M. S. Abadir,
``Formal Verification of Content Addressable Memories Using Symbolic Simulation,''
*34th Design Automation Conference DAC '97*, June, 1997,
pp. 167-172.

Y.-A. Chen, and R. E. Bryant,
``ACV: An Arithmetic Circuit Verifier,''
*International Conference on Computer-Aided Design ICCAD '96*,
November, 1996, pp. 361-365.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccad96.pdf`.

A. Jain, K. A. Nelson, and R. E. Bryant,
``Verifying Nondeterministic Implementations of Deterministic Systems,''
*Formal Methods in Computer-Aided Design FMCAD '96*,
M. Srivas and A. Camilleri, *eds.*,
LNCS 1166,
Springer-Verlag, November, 1996, pp. 109-125.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/fmcad96.pdf`.

M. Pandey, R. Raimi, D. L. Beatty, and R. E. Bryant,
``Formal Verification of PowerPC(TM) Arrays using Symbolic Trajectory Evaluation,''
*33rd Design Automation Conference*, June, 1996,
pp. 649-654.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac96a.pdf`.

R. E. Bryant,
``Bit-Level Analysis of an SRT Divider Circuit,''
*33rd Design Automation Conference*, June, 1996,
pp. 661-665.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac96b.pdf`.

R. E. Bryant,
``Binary Decision Diagrams and Beyond: Enabling
Technologies for Formal Verification,''
*International Conference on Computer-Aided Design ICCAD '95*,
November, 1995, pp. 236-243.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccad95.pdf`.

M. Pandey, A. Jain, R. E. Bryant, D. Beatty, G. York, and S. Jain,
``Extraction of finite state machines from transistor netlists by symbolic simulation,''
*International Conference on Computer Design*,
1995, pp. 596-601.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccd95.pdf`. (The postscript has problems with ghostview, but it prints OK).

R. E. Bryant, and Y.-A. Chen,
``Verification of Arithmetic Circuits with Binary Moment Diagrams,''
*32nd Design Automation Conference*, June, 1995, pp. 535-541.
Winner of best paper award in category ``Verification, Simulation, and Test.''
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac95a.pdf`.

S. Jain, R. E. Bryant, and A. Jain,
``Automatic Clock Abstraction from Sequential Circuits,''
*32nd Design Automation Conference*, June, 1995, pp. 707-711.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac95b.pdf`.

D. L. Beatty, and R. E. Bryant,
``Formally Verifying a Microprocessor using a Simulation Methodology,''
*31st Design Automation Conference*,
June, 1994, pp. 596-602.

R. E. Bryant, and C.-J. H. Seger,
``Digital Circuit Verification using Partially-Ordered State Models,''
Invited paper,
*International Symposium on Multi-Valued Logic*,
May, 1994, pp. 2-7.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/ismvl94.pdf`.

A. Jain, and R. E. Bryant,
``Inverter Minimization in Logic Networks,''
*International Conference on Computer-Aided Design*,
November, 1993, pp. 462-465.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccad93.pdf`.

R. E. Bryant, J. D. Tygar, and L. P. Huang,
``Geometric Characterization of Series-Parallel Variable Resistor
Networks,''
*International Symposium on Circuits and Systems*, May, 1993.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iscas93.pdf`.

R. E. Bryant,
``Extraction of Gate Level Models from Transistor Circuits by
Four-Valued Symbolic Analysis,''
*International Conference on Computer-Aided Design*,
November, 1991, pp. 350-353.
Reprinted in
*The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design*,
A. Kuehlmann, *ed.*
Kluwer Academic Publishers, 2003,
pp. 337-346.

Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccad91.pdf`.

R. E. Bryant, D. L. Beatty, and C.-J. H. Seger,
``Formal Hardware Verification by Symbolic Ternary Trajectory
Evaluation,''
*28th Design Automation Conference*, June, 1991, pp. 397-402.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac91a.pdf`.

A. Jain, and R. E. Bryant,
``Mapping Switch-Level Simulation onto Gate-Level Hardware Accelerators,''
*28th Design Automation Conference*, June, 1991, pp. 219-222.
Version with figures and references omitted available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac91b.pdf`.

R. E. Bryant, and C.-J. H. Seger,
``Formal Verification of Digital Circuits Using Symbolic Ternary System
Models,''
*Computer-Aided Verification '90*, E. M. Clarke, and R. P. Kurshan,
*eds.*
American Mathematical Society,
1991, pp. 121-146. Version with figures omitted available
as
`http://www.cs.cmu.edu/~bryant/pubdir/cav90.pdf`.
Also available as technical report CMU-CS-90-131.

R. E. Bryant,
``Symbolic Simulation--Techniques and Applications,''
*27th Design Automation Conference*,
June, 1990, pp. 517-521.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac90.pdf`.

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.
For those who subscribe to the IEEE Xplore publication service, you
can get an electronic copy from
`http://ieeexplore.ieee.org/iel2/790/3382/00114826.pdf?isNumber=3382`.

K. Cho, and R. E. Bryant,
``Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault
Simulation,''
*26th Design Automation Conference*,
June, 1989, pp. 418-423.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac89.pdf`.

R. E. Bryant,
``Data Parallel Switch-Level Simulation,''
*IEEE International Conference on Computer-Aided Design*,
November, 1988, pp. 354-357.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccad88.pdf`

R. E. Bryant,
``Verification of a Static RAM Design by Logic Simulation,''
*Fifth MIT Conference on Advanced Research in VLSI*,
March, 1988,
pp. 335-349.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/mit88.pdf`.

R. E. Bryant, D. Beatty, K. Brace, K. Cho, and T. Sheffler,
``COSMOS: A Compiled Simulator for MOS Circuits,''
*24th Design Automation Conference*, 1987,
pp. 9-16.
Also in
*25 Years of Electronic Design Automation*, ACM/IEEE, 1988,
pp. 496-503.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac87.pdf`.

R. E. Bryant,
``Symbolic Manipulation of Boolean Functions Using a Graphical
Representation,''
*22nd Design Automation Conference*, June, 1985,
pp. 688-694.
Electronic version with figures omitted available as
`http://www.cs.cmu.edu/~bryant/pubdir/dac85.pdf`

R. E. Bryant,
``Symbolic Verification of MOS Circuits,''
*1985 Chapel Hill Conference on VLSI*,
May, 1985, pp. 419-438.
Electronic version with figures omitted available as
`http://www.cs.cmu.edu/~bryant/pubdir/unc85.pdf`

R. E. Bryant,
``A View from the Engine Room: Computational Support for Symbolic Model Checking,''
*25 Years of Model Checking*,
H. Veith and O. Grunberg, *eds*.
LNCS-4925, Springer-Verlag, 2007,
available as
`http://www.cs.cmu.edu/~bryant/pubdir/mcxxv06.pdf`.

R. E. Bryant,
``Formal Verification of Infinite State Systems Using Boolean Methods,''
*Logic in Computer Science LICS 2006*, IEEE,
July, 2006, pp. 3-4,
available as
`http://www.cs.cmu.edu/~bryant/pubdir/lics06.pdf`,
and
*Term Rewriting and Applications RTA 2006*,
LNCS 4098, Springer-Verlag, July, 2006, pp. 1-3,
available as
`http://www.cs.cmu.edu/~bryant/pubdir/rta06.pdf`.

R. E. Bryant, S. A. Seshia,
``Decision Procedures Customized for Formal Verification,''
*Automated Deduction CADE 2005*, LNCS 3632,
Springer-Verlag, July, 2005, pp. 255-259.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cade06.pdf`.

R. E. Bryant, and S. K. Rajamani,
``Verifying Properties of Hardware and Software by Predicate Abstraction and
Model Checking,''
*International Conference on Computer-Aided Design ICCAD '04*,
November, 2004, pp. 236-243.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccad04.pdf`.

R. E. Bryant,
``System Modeling and Verification with UCLID,''
*Formal Methods and Models for Co-Design MEMOCODE '04*,
June, 2004, IEEE, June, 2004, pp. 3-4. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/memocode04.pdf`.

R. E. Bryant,
``Reasoning about Infinite-State Systems Using Boolean Methods,''
*Foundations of Software Technology and Theoretical Computer Science FSTTCS '03*, December, 2003. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/fsttcs03.pdf`.

R. E. Bryant, S. German, and M. N. Velev,
``Microprocessor Verification Using Efficient Decision Procedures
for a Logic of Equality with Uninterpreted Functions,''
*Tableaux '99*,
N. Murray, *ed.*, LNAI 1617,
Springer-Verlag,
June, 1999.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tableaux99.pdf`.

R. E. Bryant,
``Symbolic Analysis Methods for Masks, Circuits, and Systems,''
Invited paper,
*International Conference on Computer Design ICCD '93*,
October, 1993.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/iccd93.pdf`.

R. E. Bryant,
``Verification of Synchronous Circuits by Symbolic Logic Simulation,''
in *Hardware Specification, Verification, and Synthesis: Mathematical
Aspects*, M. Leeser and G. Brown, *eds*., Springer-Verlag, 1990,
pp. 14-24.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cornell89.pdf`.

R. E. Bryant, ``Introductory Computer Science Education at Carnegie Mellon University: A Deans' Perspective,''
Technical report CMU-CS-10-140. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cmu-cs-10-140.pdf`.

R. E. Bryant, ``Data-Intensive Supercomputing: The Case for DISC,''
Technical report CMU-CS-07-128. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/cmu-cs-07-128.pdf`.

R. E. Bryant, ``Term-Level Verification of a CISC Microprocessor,''
Technical report CMU-CS-05-195. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/CMU-CS-05-195.pdf`.

S. A. Seshia, and R. E. Bryant, ``The Hardness of Approximating Minima in OBDDs, FBDDs, and Boolean Functions,''
Technical report CMU-CS-00-156. Available as
`http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-156.ps`.

Y.-A. Chen, B. Yang, and R. E. Bryant,
``Breadth-First with Depth-First BDD Construction: A Hybrid Approach,''
Technical Report CMU-CS-97-120, March, 1997.
Available as
`http://reports-archive.adm.cs.cmu.edu/anon/1997/CMU-CS-97-120.ps`.

M. Starkey, and R. E. Bryant,
``Using Ordered Binary-Decision Diagrams for Compressing Images and Image Sequences,''
Technical Report CMU-CS-95-105, January, 1995.
Available as
`http://reports-archive.adm.cs.cmu.edu/anon/1995/CMU-CS-95-105.ps`.

R. E. Bryant,
``An Analysis of U.S. Patent 5,243,538 `Comparison and Verification System for Logic Circuits and Method Thereof',''
unpublished manuscript, 1994.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/patent94.pdf`.

R. E. Bryant, and Y.-A. Chen,
``Verification of Arithmetic Functions with Binary Moment Diagrams,''
Technical Report CMU-CS-94-160, May 31, 1994.
Available as
`http://reports-archive.adm.cs.cmu.edu/anon/1994/CMU-CS-94-160.ps`, and also as
`http://www.cs.cmu.edu/~bryant/pubdir/CMU-CS-94-160.pdf`.

R. E. Bryant,
*A Switch-Level Simulation Model for Integrated Logic Circuits*,
(PhD thesis), Technical Report TR-259, MIT Laboratory for Computer Science,
March, 1981.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/MIT-LCS-TR-259.pdf`.

R. E. Bryant,
*Simulation of Packet Communication Architecture Computer Systems*,
(Master's thesis), Technical Report TR-188, MIT Laboratory for Computer
Science, November, 1977.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/MIT-LCS-TR-188.pdf`.

- *11/10/12
- ``Creating a Foundational Curriculum in Computer Science,''
University Course Forum in Computer Science,
Guangzhou, China
- *9/19/11
- ``Computer Science Research Opportunities in Sustainability,''
US-China Collaborations in Computer Science and Sustainability,
DIMACS, Rutgers.
- *6/8/11
- ``Data-Intensive Scalable Computing,''
Workshop on Building Blocks for Scalable Cloud Computing, Design Automation Conference,
San Diego, CA.
- *4/14/11
- ``Data-Intensive Scalable Computing,''
Teragrid/Blue Waters Symposium, Pittsburgh, PA.
- *06/24/10
- ``Data-Intensive Scalable Computing: Finding the Right Programming Models.''
Keynote presentation, High-Performance and Distributed Computing Conference,
Chicago, IL.
- 01/29/10
- ``Data-Intensive Scalable Computing: Prospects and Challenges.''
OpenCirrus Consortium, Sunnyvale, CA.
- 10/16/09
- ``Data-Intensive Scalable Computing for eScience,''
Microsoft eScience Workshop,
Pittsburgh, PA.
- *10/13/09
- ``Data-Intensive Scalable Computing,'' Los Alamos Computer Science
Symposium, Santa Fe, NM.
- 07/30/09
- ``Data-Intensive Computing: The Prospects and the Challenges,''
Workshop on Enabling Data-Intensive Computing: from Systems to
Applications, University of Pittsburgh, Pittsburgh, PA.
- 6/25/08
- ``Data-Intensive Cloud Computing,'' as part of panel session on Cloud
Computing at the High-Performance Distributed Computing Conference,
Boston, MA.
- *4/23/08
- ``Reasoning about Data: Bits, Bit Vectors, or Words,''
Keynote Speech, International Symposium on VLSI Design Automation, and Test,
Hsinchu, Taiwan.
- *3/26/08
- ``Data-Intensive Super Computing,''
Symposium on Data-Intensive Computing, Sunnyvale, CA.
- *3/17/08
- ``Data-Intensive Super Computing,''
Technology@Sun 2008 (an internal meeting of the engineering leadership of Sun Microsystems, Santa Cruz, CA.
- *11/11/07
- ``Modeling Data in Formal Verification: Bits, Bit Vectors, or Words,''
Tutorial at Formal Methods in Computer-Aided Design, Austin, TX.
- *6/13/07
- ``Data-Intensive Super Computing: Taking Google-Style Computing Beyond Web Search,''
Special session at Federated Computing Research Conference, San Diego, CA.
- *8/16/06
- ``A View from the Engine Room: Computational Support for Symbolic Model Checking,'' Workshop on 25 Years of Model Checking, Seattle, WA.
- *8/12/06
- ``Formal Verification of Infinite State Systems using Boolean Methods,''
Plenary talk, Federated Logic Conference, Seattle, WA.
- *7/26/05
- ``Decision Procedures Customized for Formal Verification,''
Conference on Automated Deduction (CADE), Tallinn, Estonia
- 11/9/04
- ``Symbolic, Word-Level Hardware Verification,''
Embedded tutorial, ICCAD '04, San Jose, CA.
- *6/23/04
- ``System Modeling and Verification with UCLID,''
Keynote talk,
Formal Methods and Models for Co-Design,
San Diego, CA.
- *12/15/03
- ``Reasoning about Infinite-State Systems Using Boolean Methods,''
Keynote talk,
Foundations of Software Technology and Theoretical Computer Science,
Mumbai, India.
- 12/14/03
- ``SAT-Based Decision Procedures for Subsets of First-Order Logic,''
Workshop on Model Checking, Mumbai, India.
- *11/2/02
- ``Symbolic Simulation and its Connection to Formal Verification,''
Formal Methods in Computer-Aided Design,
Portland, Oregon
- *6/3/02
- ``Introducing Computer Systems from a Programmer's Perspective,''
David C. Evans Conference on Computer Engineering,
Utah
- *5/00
- ``Binary Decision Diagrams and Symbolic Model Checking,''
Symposium on Algorithms in the Real World,
Pittsburgh, PA
- 7/10/99
- ``Exploiting Positive Equality in a Logic of Equality
With Uninterpreted Functions,''
Computer-Aided Verification,
CAV '99, Trento Italy.
- 7/9/99
- ``Optimizing Symbolic Model Checking for Constraint-Rich Models,''
Computer-Aided Verification,
CAV '99, Trento Italy.
- *6/8/99
- ``Microprocessor Verification Using Uninterpreted Functions,''
Tableaux '99, Saratoga Springs, NY.
- *4/2/98
- ``Formal Verification of Pipelined Processors,''
European Joint Conferences on Theoretical and Practical Aspects of Software,
Lisbon, Portugal.
- *12/11/97
- ``Formal Verification of Pipelined Processors,''
Third Asian Computing Science Conference,
Kathmandu, Nepal.
- 6/24/97
- ``Exploiting Symmetry When Verifying Transistor Circuits by Symbolic
Trajectory Evaluation,'' Computer-Aided Verification, CAV '97, Haifa Israel.
- 6/6/96
- ``Bit-Level Analysis of an SRT Divider Circuit,''
32nd Design Automation Conference, Las Vegas CA.
- 3/25/96
- ``BDDs and Beyond: Enabling Technologies for Formal Verification,''
DIMACS Workshop on Formal Verification.
- 3/11/96
- ``BDDs Applied to SAT and Related Problems,''
DIMACS Workshop on Satisfiability, Rutgers University.
- 11/6/95
- ``BDDs and Beyond: Enabling Technologies for Formal Verification,''
Embedded tutorial, ICCAD '95, San Jose, CA.
- *7/3/95
- ``Multipliers and Dividers: Insights on Arithmetic Circuit Verification,''
Computer-Aided Verification, CAV '95, Liege, Belgium.
- 2/17/95
- ``Formal Verification of Arithmetic Circuits with Binary Moment Diagrams,''
Computer Systems Seminar,
Dagstuhl Seminar on Computer-Aided Design, Dagstuhl, Germany.
- *5/25/94
- ``Digital Circuit Verification using Partially-Ordered State Models,''
24th International Symposium on Multiple-Valued Logic, Boston, MA.
- *11/29/93
- ``Symbolic Analysis Methods for Masks, Circuits, and Systems,''
GMD 25th Anniversary Symposium, Bonn, Germany.
- 11/4/93
- ``Beyond Digital CAD: New Applications for Binary Decision Diagrams,''
ARPA Microsystem Contractors Meeting, Seattle, WA.
- *10/4/93
- ``Symbolic Analysis Methods for Masks, Circuits, and Systems,''
CAD
Plenary Session, International Conference on Computer Design, Cambridge, MA.
- 5/93
- ``Geometric Characterization of Series-Parallel Variable Resistor Networks,''
International Symposium on Circuits and Systems, Chicago, IL.
- *3/26/92
- ``Privileged but Illiterate, Report on a Year in Japan,''
MIT/Brown Conference on Advanced Research in VLSI and Parallel
Systems, Providence, RI.
- 11/14/91
- ``Privileged but Illiterate, Report on a Year in Japan,''
DARPA VLSI Contractors Meeting, Pasadena, CA.
- 11/12/91
- ``Extraction of Gate Level Models
from Transistor Circuits by 4-Valued Symbolic Analysis.''
International Conference on Computer-Aided Design, Santa Clara, CA.
- *6/19/91
- ``Formal Verification, a Slow, but Certain Evolution,''
Panel on Formal Methods, 28th Design Automation Conference.
- 2/4/91
- ``Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams,''
Second Makuhari Conference on High Technology, Chiba, Japan.
- *10/24/90
- ``Formal Hardware Verification by Symbolic
Simulation,'' 1990 Synthesis and Simulation Meeting and International
Interchange, Kyoto, Japan.
- *8/31/90
- ``Symbolic Simulation--Techniques and Applications,''
Japanese Design Automation Workshop, Gamagouri, Japan.
- 6/27/90
- ``Symbolic Simulation--Techniques and Applications,''
27th Design Automation Conference.
- *11/15/89
- ``Symbolic Analysis and Verification of MOS Circuits,''
IFIP Workshop on Applied Formal Methods for Correct VLSI Design,
Hengelhoef, Belgium.
- *7/5/89
- ``Verification of Synchronous Circuits by Symbolic Logic Simulation,''
Workshop on Hardware Specification, Verification, and Synthesis,
Cornell University.
- 6/27/89
- ``Test Pattern Generation for Sequential MOS Circuits by
Symbolic Fault Simulation,'' 26th Design Automation Conference.
- *5/8/89
- ``Physical/Functional Tool Integration,'' panel discussion at
1989 Synthesis and Simulation Meeting and International Interchange, Osaka, Japan.
- 4/3/89
- ``Test Pattern Generation for Combinational and Sequential MOS Circuits by
Symbolic Fault Simulation,''
DARPA VLSI Contractor's Meeting, Snowbird, UT.
- 11/9/88
- ``Data Parallel Switch-Level Simulation,''
International Conference on Computer-Aided Design.
- 6/15/88
- ``CAD Tool Needs for System Designers,''
Panel Session Chairman, 25th Design Automation Conference.
- 3/30/88
- ``Verifying a Static RAM Design by Logic Simulation,''
Fifth MIT Conference on Advanced Research in VLSI.
- 2/1/88
- ``Verifying a Static RAM Design by Logic Simulation,''
IEEE VLSI Workshop, Clearwater Beach, FL.
- 11/16/87
- ``COSMOS Makes its Debut,''
DARPA VLSI Contractors Meeting, Berkeley, CA.
- *9/15/87
- ``Transistor-Level Logic Simulation,''
Semiconductor Research Conference Topical Research Conference on Design Verification,
Pittsburgh, PA.
- 6/29/87
- ``COSMOS: A Compiled Simulator for MOS Circuits,''
24th Design Automation Conference, Miami Beach, FL.
- *5/26/87
- ``Symbolic Analysis of MOS Circuits,''
U.S./Israel Joint Workshop on VLSI Architecture and Design,
Tiberias, Israel.
- 2/24/87
- ``COSMOS: A Compiled Simulator for MOS Circuits,''
IEEE VLSI Workshop, Clearwater Beach, FL.
- *10/28/86
- ``Compiled Simulation of MOS Circuits,'' Canadian
Conference on VLSI, Montreal.
- 10/1/85
- ``Formal Verification of Digital Circuits by Logic Simulation,''
DARPA VLSI Contractors Meeting, Seattle, WA.
- *7/2/85
- ``Can a Simulator Verify a Circuit?,''
Workshop on Formal Aspects of VLSI, Edinburgh University, Scotland.
- 6/27/85
- ``Performance Evaluation of FMOSSIM: a Concurrent, Switch-Level
Fault Simulator,''
22nd Design Automation Conference, Las Vegas, Nevada.
- 6/27/85
- ``Symbolic Manipulation of Boolean Functions Using a Graphical
Representation,''
22nd Design Automation Conference, Las Vegas, Nevada.
- 5/17/85
- ``Symbolic Verification of MOS Circuits,''
1985 Chapel Hill Conference on VLSI, Chapel Hill, North Carolina.
- 4/24/85
- ``Test Generation for MOS Circuits by Symbolic Fault Simulation,''
IEEE Workshop on Design for Testability, Beaver Creek, Colorado.
- 3/18/85
- ``Symbolic Verification of MOS Circuits,''
DARPA VLSI Contractors Meeting, Salt Lake City, UT.
- *10/84
- ``Simulators (Will Always) Provide Superior Models,''
Panel on Testability Measures,
1984 International Test Conference, Philadelphia, Pennsylvania.
- *4/84
- ``Experiments with a Switch-Level Fault Simulator,''
IEEE Workshop on Design for Testability, Vail, Colorado.
- *11/28/83
- ``Switch-Level Models for MOS Digital Systems,''
Mathematical Methods of VLSI, Mathematisches Forschungsinstitut,
Oberwolfach, Germany.
- 8/16/83
- ``Race Detection in MOS Circuits by Ternary Simulation,''
VLSI 83, Trondheim, Norway.
- *6/28/83
- ``The Role of Simulation in VLSI Design,''
VLSI for the 80's, Victoria B. C., Canada.
- *4/25/83
- ``Switch-Level Fault Simulation,''
IEEE West Coast Test Workshop,
Napa, Calif.
- *5/10/82
- ``Switch-Level Modeling of MOS Digital Circuits,''
IEEE International Symposium on Circuits and Systems,
Rome, Italy.
- 8/21/81
- ``A Switch-Level Model of MOS Logic Circuits,''
VLSI 81, Edinburgh, Scotland.
- 7/1/81
- ``MOSSIM: A Logic Simulator for MOS LSI,''
18th Design Automation Conference,
Nashville, Tennessee.
- 10/5/79
- ``Simulation on a Distributed System,''
First International Conference on Distributed Systems,
Huntsville, Ala.
- 7/78
- ``Analytical Models of Interconnection Networks,'' Workshop on Data Flow Computer and Program Organization, Dedham, MA.

- 11/9/12
- ``Creating a Foundational Curriculum in Computer Science,''
University of Science and Technology Beijing.
- 10/24/12
- ``Data Intensive Scalable Computing,''
Karlsruhe Institute of Technology, Karlsruhe, Germany
- 6/7/12
- ``Introducing Computer Systems from a Programmer's Perspective,''
Tsinghua University, Beijing, China.
- 6/5/12
- ``Data Intensive Scalable Computing,''
Peking University, Beijing, China.
- 6/4/12
- ``Introducing Computer Systems from a Programmer's Perspective,''
Peking University, Beijing, China.
- 2/3/12
- ``Introducing Computer Systems from a Programmer's Perspective,''
Strathmore University, Nairobi, Kenya.
- 2/1/12
- ``Data-Intensive Scalable Computing: Finding the Right Programming Model''
Computer Science Seminar,
Carnegie Mellon Qatar Campus.
- 1/31/12
- ``Data-Intensive Scalable Computing,'' Nico Habermann Memorial Lecture,
Carnegie Mellon Qatar Campus.
- 3/16/11
- ``Data-Intensive Scalable Computing: Finding the Right Programming Model,''
Distinguished Lecture, Northwestern University Computer Science Department.
- 3/9/11
- ``Data-Intensive Scalable Computing: Finding the Right Programming Model,''
Los Alamos National Laboratory.
- 11/4/09
- ``BDDs and SAT Solvers: Applying Boolean Reasoning to Formal Hardware Verification,''
Cadence Design Systems, Sunnyvale, CA.
- 1/6/09
- ``Data-Intensive Scalable Computing: Taking Google-Style Computing Beyond Web Search,''
National University of Singapore, Singapore.
- 1/5/09
- ``Data-Intensive Scalable Computing: Taking Google-Style Computing Beyond Web Search,''
Nanyang Technical University, Singapore.
- 11/14/08
- ``Data-Intensive Scalable Computing: Taking Google-Style Computing Beyond Web Search,''
University of Kentucky, Computer Science Department Distinguished Lecture.
- 10/20/08
- ``Data-Intensive Scalable Computing: Taking Google-Style Computing Beyond Web Search,''
RAND Corporation, Washington DC.
- 10/20/08
- ``Data-Intensive Scalable Computing: Taking Google-Style Computing Beyond Web Search,''
National Science Foundation, CISE Distinguished Lecture.
- 10/14/08
- ``Data-Intensive Scalable Computing: Taking Google-Style Computing Beyond Web Search,''
Oxford University Strachey Distinguished Lecture, Oxford, England.
- 10/03/08
- ``Data-Intensive Scalable Computing: Taking Google-Style Computing Beyond Web Search,''
University of Michigan, Computer Science and Engineering Seminar.
- 05/05/08
- ``Data-Intensive Scalable Computing: Taking Google-Style Computing Beyond Web Search,''
Carnegie Mellon University Qatar Campus.
- 3/21/08
- ``Data-Intensive Super Computing: Taking Google-Style Computing Beyond Web Search,''
Barr Systems Lecture Series, University of Florida.
- 3/10/08
- ``Data-Intensive Super Computing: Taking Google-Style Computing Beyond Web Search,''
IT Eminent Lecture Series, Louisiana State University.
- 11/14/07
- ``Data-Intensive Super Computing: Taking Google-Style Computing Beyond Web Search,''
Kent State University, Kent, OH.
- 1/12/07
- ``Bit-Vector Decision Procedures: A Basis for Reasoning about Hardware and Software,''
Microsoft Research, Redmond, WA.
- 1/3/07
- ``Automated Formal Verification of Software: Status and Prospects,''
Department of Computer Science, National University of Singapore.
- 5/26/06
- ``Computer Systems: A Programmer's Perspective,''
Southeast University,
Nanjing, China.
- 2/8/06
- ``Verifying Infinite-State Systems Using Boolean Methods,''
MIT CSAIL Michael Dertouzos Distinguished Lecture, MIT.
- 7/12-14/05
- Seminars at Intel in Haifa, Israel:
- ``SAT-Based Decision Procedures for Linear Arithmetic and Uninterpreted Functions''
- ``System Modeling and Verification with UCLID''
- ``Symbolic Approaches to Invariant Checking and Automatic Predicate Abstraction''

- 6/7/05
- ``Binary Decision Diagrams and Their Applications,''
Information and Communications University,
Daejeon, Korea.
- 9/5/04
- ``Binary Decision Diagrams and Their Applications,''
Kuwait University Department of Math and Computer Science.
- 9/3/04
- ``SAT-Based Decision Procedures for Subsets of First-Order Logic,''
Kuwait University Department of Math and Computer Science.
- 8/19/04
- ``Reasoning about Infinite-State Systems Using Boolean Methods,''
Distinguished Lecture,
Cadence Corporation,
San Jose, CA.
- 4/26/04
- ``Verifying Infinite-State Systems Using Boolean Methods,''
Harvard University.
- 4/14/04
- ``Verifying Infinite-State Systems Using Boolean Methods,''
Distinguished Lecture, Southern Methodist University.
- 10/23/03
- ``Verifying Infinite-State Systems Using Boolean Methods,''
Distinguished Lecture, University of Pennsylvania Computer Science Department.
- 7/14/03
- ``Verifying Infinite-State Models Using Boolean Methods,''
Synopsys, Inc., Hillsboro, OR.
- 4/21/03
- ``Formal Verification Using Infinite-State Models,''
Fujitsu Laboratories, Kawasaki, Japan.
- 3/6/03
- ``Formal Verification Using Infinite-State Models,''
Distinguished Lecture, UCLA Computer Science Department.
- 11/14/02
- ``Introducing Computer Systems from a Programmer's
Perspective,''
Distinguished Lecture, School of Computing, Georgia
Institute of Technology, Atlanta, Georgia.
- 7/13/99
- ``Optimizing Symbolic Model Checking for Constraint-Rich Models,''
IBM Haifa Research Laboratory, Haifa, Israel.
- 7/12/99
- ``Processor Verification Using Efficient Reductions of the Logic of
Uninterpreted Functions to Propositional Logic,''
Intel Logic Verification Symposium, Haifa, Israel.
- 6/26/98
- ``Bit-Level Verification of Pipelined Processors,''
Intel Corp., Hillsboro, OR.
- 3/26/97
- ``Hierarchical Verification Based on Symbolic Trajectory Evaluation''
Lucent Technologies Bell Laboratories, Murray Hill, NJ
- 12/6/96
- ``Hierarchical Verification based on Symbolic Trajectory Evaluation''
Intel Corp., Hillsboro, OR.
- 10/24/96
- ``Multipliers and Dividers, Insights on Arithmetic Circuit Verification,''
Distinguished Lecture, Department of Computer Science, University of
Washington.
- 4/12/96
- ``Formal Verification of Sequential Processors'',
Intel Frontiers in CAD Symposium, Hillsboro, OR.
- 2/22/96
- ``Multipliers and Dividers, Insights on Arithmetic Circuit Verification,''
Distinguished Lecture, Department of Computer Science, University of Utah.
- 12/4/95
- ``Division Pentium Style: An Analysis of Intel's Mistake(s),''
Distinguished Speaker Series,
Cadence Design Systems, Chelmsford, MA.
- 11/8/95
- ``Multipliers and Dividers, Insights on Arithmetic Circuit Verification,''
SRI International, Menlo Park, CA.
- 10/11/95
- ``Multipliers and Dividers, Insights on Arithmetic Circuit Verification,''
EECS CAD Seminar, U. C. Berkeley.
- 7/17/95
- ``Multipliers and Dividers, Insights on Arithmetic Circuit Verification,''
EECS Dept., University of Michigan.
- 4/21/95
- ``Formal Verification of Arithmetic Circuits with Binary Moment Diagrams,''
Distinguished Lecture, University of Southern California.
- 2/22/95
- ``Division Pentium Style: An Analysis of Intel's Mistake(s),''
Computer Systems Seminar,
Carnegie Mellon University Computer Science Department.
- 10/21/94
- ``Formal Verification of Arithmetic Circuits with Binary Moment Diagrams,''
Computer Systems Seminar,
Carnegie Mellon University Computer Science Department.
- 10/5/94
- ``Formal Verification of Arithmetic Circuits with Binary Moment Diagrams,''
Distinguished Lecture, University of Texas
Computer Science Department.
- 10/3/94
- ``Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams,''
Distinguished Lecture, University of Texas
Computer Science Department.
- 12/1/93
- ``Symbolic Analysis Methods for Masks, Circuits, and Systems,''
University of Trier, Trier, Germany.
- 5/93
- ``A Methodology for Formal Hardware Verification, with Application to
a Real Microprocessor,''
University of Grenoble, Grenoble, France.
- 5/93
- ``A Methodology for Formal Hardware Verification, with Application to
a Real Microprocessor,''
Digital Equipment Corp., Paris Research Laboratory, Paris, France.
- 10/30/92
- ``Formal Hardware Verification by Symbolic
Trajectory Evaluation,'' Motorola Corp., Austin, TX.
- 10/29/32
- ``Formal Hardware Verification by Symbolic
Trajectory Evaluation,'' IBM Corp., Austin, TX.
- 7/14/92
- ``Formal Hardware Verification by Symbolic
Trajectory Evaluation,'' Intel Corp., Hillsboro, OR.
- 3/3/92
- ``Formal Hardware Verification and Logic Abstraction,''
Digital Equipment Corporation, Hudson, MA.
- 3/2/92
- ``Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams,''
Harvard University.
- 5/23/91
- ``Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams,''
Fujitsu International Institute for Advanced
Study of Social Information Science, Numazu, Japan.
- 5/22/91
- ``Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams,''
Tokyo Institute of Technology, Tokyo, Japan.
- 5/20/91
- ``Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams,''
Kyushu Institute of Technology, Iizuka, Japan.
- 5/13/91
- ``Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams,''
Fujitsu Laboratories, Kawasaki, Japan.
- 5/9/91
- ``Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams,''
Dept. of Information Science, Kyoto University, Kyoto, Japan.
- 3/15/91
- ``Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams,''
Nippon Electric Corporation, Kawasaki, Japan.
- 3/15/91
- ``The COSMOS Project: Switch-Level Modeling and Simulation,''
Nippon Electric Corporation, Kawasaki, Japan.
- 3/1/91
- ``Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams,''
Electrotechnical Laboratory, Tsukuba, Japan.
- 6/8/90
- ``Formal Verification of MOS Circuits by Symbolic
Simulation,''
Siemens AG, Munich, Germany.
- 6/5/90
- ``Formal Verification of MOS Circuits by Symbolic
Simulation,''
Bull Research Center, Paris, France.
- 10/23/89
- ``The COSMOS Project: Switch-Level Modeling and Simulation,''
Gateway Design Automation Corp., Lowell, MA.
- 6/7/89
- ``Test Pattern Generation for Sequential MOS Circuits by
Symbolic Fault Simulation,''
Hewlett Packard, Palo Alto, CA.
- 6/2/89
- ``Test Pattern Generation for Sequential MOS Circuits by
Symbolic Fault Simulation,''
General Electric, Schenectady, NY.
- 5/11/89
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
Fujitsu Laboratories, Kawasaki, Japan.
- 5/10/89
- ``Switch-Level Simulation,'' Matsushita Electric Industrial
Co., Osaka Japan.
- 1/20/89
- ``Graph-Based Algorithms for Boolean Function Manipulation,''
University of Colorado.
- 11/7/88
- ``Test Pattern Generation for Sequential MOS Circuits by
Symbolic Fault Simulation,''
CAD Seminar, University of California, Berkeley.
- 11/3/88
- ``Test Pattern Generation for Sequential MOS Circuits by
Symbolic Fault Simulation,''
CMU Center or Dependable Systems Seminar.
- 10/20/88
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
Syracuse University.
- 7/18/88
- ``Graph-Based Algorithms for Boolean Function Manipulation,''
IBM Watson Research Center, Yorktown Hts., NY.
- 6/9/88
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
Digital Equip. Corp., Hudson, MA.
- 4/22/88
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
University of Illinois, Coordinated Sciences Laboratory.
- 4/13/88
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
University of Waterloo, Ontario.
- 3/8/88
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
MIT VLSI Seminar.
- 11/18/87
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
Xerox Palo Alto Research Center.
- 11/17/87
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
CAD Seminar, University of California, Berkeley.
- 5/13/87
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
Dept. Elec. Eng., Texas A&M Univ.
- 4/10/87
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
VLSI Seminar, IBM Watson Research Center, Yorktown Hts., NY.
- 1/30/87
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
Computer Systems Seminar, Carnegie Mellon University.
- 12/18/86
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
Dept. Comp. Sci., Univ. of Washington.
- 12/18/86
- ``Fault Simulation of MOS Circuits,''
Dept. Comp. Sci., Univ. of Washington.
- 12/1/86
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
AT&T Bell Laboratories, Murray Hill, NJ.
- 10/29/86
- ``Formal Verification of Digital Circuits by Logic
Simulation,'' Dept. Elec. Engineering, McGill University, Montreal, Canada.
- 10/21/86
- ``COSMOS: A COmpiled Simulator for MOS Circuits,''
Design Automation Seminar, CMU Dept. Electrical and Computer Engineering.
- 3/4/86
- ``Symbolic Verification of MOS Circuits,''
Computer Science Seminar, Caltech.
- 1/28/86
- ``Formal Verification of Digital Circuits by Logic Simulation,''
Computer Science Seminar, Univ. of Utah.
- 11/6/85
- ``Formal Verification of Digital Circuits by Logic Simulation,''
Computer Science Seminar, Univ. of Waterloo, Ontario.
- 10/22/85
- ``Symbolic Verification of MOS Circuits,''
VLSI Seminar, MIT Dept. of EECS.
- 10/4/85
- ``Symbolic Verification of MOS Circuits,''
Stanford Dept. of Elec. Eng.
- 10/3/85
- ``Symbolic Verification of MOS Circuits,''
Schlumberger Research, Palo Alto, CA.
- 6/12/85
- ``Symbolic Methods for MOS Circuits,''
Texas Instruments, Dallas, TX.
- 4/23/85
- ``Symbolic Verification of MOS Circuits,''
ECE Dept. Univ. of Colorado.
- 11/30/84
- ``Graph-Based Algorithms for Boolean Function Manipulation,''
AT&T Bell Laboratories, Murray Hill, N.J.
- 11/29/84
- ``A Switch-Level Model of MOS Circuits,''
AT&T Bell Laboratories, Murray Hill, N.J.
- 6/84
- ``The MOSSIM Simulation Engine,''
Dept. Comp. Sci., Univ. of Washington.
- 6/84
- ``Experiments with a Switch-Level Fault Simulator,''
Boeing Corp., Seattle, WA.
- 6/84
- ``The MOSSIM Simulation Engine,''
Tektronix, Inc., Portland, OR.
- 6/84
- ``The MOSSIM Simulation Engine,''
Intel Corp., Santa Clara, CA.
- 12/6/83
- ``Concurrent Fault Simulation of MOS Digital Circuits,''
Universität des Saalandes, Saarbr 0ucken, Germany.
- 11/3/83
- ``Switch-Level Simulation,''
Texas Instruments, Dallas, TX.
- 6/26/83
- ``Switch-Level Simulation,''
Intel Corp., Santa Clara, CA.
- 5/7/83
- ``Introduction to VLSI,''
California Polytechnical Institute, Pomona, CA.
- 10/20/82
- ``Architectures for VLSI,''
Fairchild Research Laboratories, Palo Alto, CA.
- 10/19/82
- ``Switch-Level Simulation and the Verification of MOS Digital
Circuits,''
UCLA Computer Science Seminar, Los Angeles, CA.
- 9/21/82
- ``Switch-Level Simulation and the Verification of MOS Digital
Circuits,''
VLSI Seminar, MIT Dept. of EECS.
- 9/20/82
- ``Switch-Level Simulation and the Verification of MOS Digital
Circuits,''
Digital Equip. Corp., Hudson, MA.
- 4/26/82
- ``A Switch-Level Model of MOS Circuits,''
IBM Watson Research Center,
Yorktown Hts., NY.
- 2/16/82
- ``A Switch-Level Model of MOS Circuits,''
Oregon Graduate Center, Hillsboro, OR.
- 4/14/80
- ``MOSSIM: A Logic Simulator for MOS LSI,''
IBM Watson Research Center,
Yorktown Hts., NY.

- 1/30/12
- ``Boolean Methods,''
Student workshop, Carnegie Mellon Qatar Campus.
- 07/29/10
- ``Boolean Methods,''
Andrew's Leap Program, Pittsburgh, PA.
- 11/06/09
- ``Computers and Robots,''
KIPP LA Prep middle school,
Los Angeles, CA.
- 11/05/09
- ``Computers and Robots,''
Locke High School, Los Angeles, CA.
- 07/08/09
- ``Data-Intensive Scalable Computing,''
Andrew's Leap Program, Pittsburgh, PA.
- 07/11/08
- ``Data-Intensive Scalable Computing,'' Andrew's Leap Program, Pittsburgh, PA.

- 2013
- Jirí Šimša, CMU CS (jointly advised by Garth Gibson). Now at Google.
- 2005
- Sanjit Seshia, CMU CS. Now on the faculty at U. C., Berkeley.
- 2004
- Miroslav Velev, CMU ECE. Now independent consultant.
- 2004
- Shuvendu Lahiri, CMU ECE. Now at Microsoft Research.
- 2004
- Amit Goel, CMU ECE. Now at Calypto Design Systems.
- 2003
- Rune Jensen, CMU CS (jointly advised by Manuela Veloso). Now on the faculty at IT University of Copenhagen.
- 2001
- Clayton McDonald. Now at Synopsys, Inc.
- 1999
- Kyle Nelson, CMU ECE.
- 1997
- Alok Jain, CMU ECE. Now at Cadence Design Systems.
- 1998
- Yirng-An Chen, CMU CS.
- 1997
- Manish Pandey, CMU CS. Now at Nutanix, Inc.
- 1993
- Derek Beatty, CMU CS. Now at Oracle.
- 1992
- Karl Brace, CMU ECE. Now at Intel Corporation.
- 1992
- Tom Sheffler, CMU ECE.
- 1991
- Larry Huang, CMU ECE.
- 1989
- Saul Kravitz, CMU ECE (jointly advised by Rob Rutenbar). Now at Howard Hughes Medical Institute.
- 1988
- Kyeongsoon Cho, CMU ECE. Now on the faculty at Hankuk University of Foreign Studies, Korea.

- 2014
- Adam Blank, CMU CS. Now at U. Washington.
- 1998
- Vishnu Patankar, CMU ECE. Now at Amazon.
- 1994
- Samir Jain, CMU ECE. Now at Honeywell.
- 1984
- Michael Schuster, Caltech CS. Now at Adobe Systems.
- 1984
- Wen-Chi Chen, Caltech CS. Now President of VIA Technologies, Inc., Taiwan.
- 1984
- Yen-Jen Oyang, Caltech CS. Now on the faculty at National Taiwan University.
- 1983
- Jimmy Lam, Caltech CS.

- 2013
- Will Klieber, CMU CS Ph.D.
- 2013
- Thangavel Bhuvaneswari, Multimedia University, Melaka, Malaysia, CS Ph.D.
- 2012
- Sicun Gao, CMU Pure and Applied Logic Ph.D.
- 2008
- David Brumley, CMU CS Ph.D.
- 2007
- Pankaj Chauhan, CMU CS Ph.D.
- 2006
- Murali Talupur, CMU CS Ph.D.
- 2006
- Anubhav Gupta, CMU CS Ph.D.
- 2006
- Alberto Oliveras, Technical University of Catalonia, Barcelona Spain, CS Ph.D.
- 2006
- Zhong Xiu, CMU ECE Ph.D.
- 2005
- Sagar Chaki, CMU CS Ph.D.
- 2004
- Hui Xu, CMU ECE Ph.D.
- 2003
- Noppanunt Utamaphethai, CMU ECE Ph.D.
- 2003
- Dong Wang, CMU ECE Ph.D.
- 2003
- Chris Wilson, Stanford University, CS Ph.D.
- 2001
- Sergei Berezin, CMU CS Ph.D.
- 2001
- Marius Minea, CMU CS Ph.D.
- 2000
- Yuan Lu, CMU ECE Ph.D.
- 2000
- Rony Kay, CMU ECE Ph.D.
- 1999
- Bwolen Yang, CMU CS Ph.D.
- 1998
- Margaret Reid-Miller, CMU CS Ph.D.
- 1997
- Mukund Sivaraman, CMU ECE Ph.D.
- 1997
- Derek Noonburg, CMU ECE Ph.D.
- 1997
- Denis Zampuniéris, Universitaires Notre-Dame de la Paix, Namur, Belgium, CS Ph.D.
- 1996
- Xudong Zhao, CMU CS Ph.D.
- 1994
- Samir Naik, CMU ECE Ph.D.
- 1994
- Aarti Gupta, CMU CS Ph.D.
- 1993
- Ken McMillan, CMU CS Ph.D.
- 1993
- Jean-Christophe Madre, Habilitation, Université Joseph Fourier, Grenoble, France.
- 1993
- David Long, CMU CS Ph.D.
- 1991
- Tom Storey, CMU ECE Ph.D.
- 1991
- John Willis, CMU ECE Ph.D.
- 1991
- Jerry Burch, CMU CS Ph.D.
- 1991
- Erik Brunvand, CMU CS Ph.D.
- 1990
- Phil Nigh, CMU ECE Ph.D.
- 1990
- Jean-Christophe Madre, Ph.D., Ecole Nationale Supérieure de Télécommunication, Paris, France.
- 1989
- Larry Pillage, CMU ECE Ph.D.
- 1989
- David Geiger, CMU ECE Ph.D.
- 1989
- David Dill, CMU CS Ph.D.
- 1987
- Carl Seger, Univ. Waterloo, Canada, CS Ph.D.
- 1986
- William Dally, Caltech CS Ph.D.
- 1985
- Ed Frank, CMU CS Ph.D.
- 1984
- Tzu-Mu Lin, Caltech CS Ph.D.
- 1983
- Erik P. DeBenedictis, Caltech CS Ph.D.
- 1982
- Charles Lang, Caltech CS Ph.D.

- 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
- Board of Session, Bellefield Presbyterian Church, Pittsburgh, PA.
- 1986-1990
- Board of Trustees, Bellefield Presbyterian Church, Pittsburgh, PA.

Randy Bryant 2015-08-03