next_inactive up previous


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

2004-present
Dean, School of Computer Science, Carnegie Mellon University.

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.

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

Google Scholar Citation Count. Downloaded 15-Apr-2014.

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

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

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

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

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

  10. R. E. Bryant, and D. R. O'Hallaron, Computer Systems: A Programmer's Perspective, Second Edition, Prentice-Hall, 2011.
    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 240 institutions worldwide.

Professional Activities

Affiliations

2011-present
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-present
Council member, Computing Community Consortium.

2010-present
American Academy of Arts and Sciences.

2010-present
Technical Advisor Board, Reveal Design Automation

2006-2012
Technical Advisory Board, NextOp Software (acquired by Atrenta, Inc.)

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

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.

Awards

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

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

Conference Committees

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.

Proposal Review Committees

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

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.

Partial List of Publications

Note: Only recent and particularly important publications are shown. If you really want to see my complete list of publications, it is available online as http://www.cs.cmu.edu/~bryant/pubs.ps, or as http://www.cs.cmu.edu/~bryant/pubs.pdf,

Books and Book Chapters

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.

Refereed Journal and Book Articles

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.

Refereed Conference Articles

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

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

Unrefereed Articles

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.

Unpublished

R. E. Bryant, ``Introductory Computer Science Education at Carnegie Mellon University: A Dean's 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.

Technical Presentations

Professional Meetings and Conferences

Invited talks indicated with asterisk.

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

Seminars and Colloquia

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:

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.

Outreach

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.

Students

Ph.D. Advisees

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. Now at Weemo.
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.

MS Advisees

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.

Thesis Committees

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.

Community Service

2001-present
Board of Directors, Steel City Rowing Club, Pittsburgh, PA. Board president 2005-present.
1998-2000, 2003-2006
Board of Session, Bellefield Presbyterian Church, Pittsburgh, PA.
1986-1990
Board of Trustees, Bellefield Presbyterian Church, Pittsburgh, PA.


next_inactive up previous
Randal E Bryant 2014-04-15