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

2014-present: Assistant Director for Information Technology Research and Development, White House Office of Science and Technology Policy
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.

Publication and Research Highlights

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

Most Cited Publications

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.
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.
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 250 institutions worldwide. The third edition will be coming out in 2015.

Professional Activities

Affiliations

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

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.

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, Third Edition, Prentice-Hall, 2015. More information available at http://csapp.cs.cmu.edu/.

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

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

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

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:

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

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

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.

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

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 2014-11-05