Randal E. Bryant

Education

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

Employment

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

Publication and Research Highlights

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

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.
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 D. R. O’Hallaron, Computer Systems: A Programmer’s Perspective, Prentice-Hall. First edition 2003, second edition 2011, third edition 2015.

A textbook based on a course created at CMU that covers the combination of hardware, networking, and software that comprises a computer system. This book has been translated into Chinese, Russian, Korean, and Macedonian, and is in use at over 325 institutions worldwide.
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.
R. E. Bryant, and Y.-A. Chen, “Verification of Arithmetic Circuits with Binary Moment Diagrams,” 32nd Design Automation Conference, June, 1995, pp. 535–541.

Describes a variant on BDDs that can represent the word-level functionality of arithmetic circuits. Winner of best paper award in category “Verification, Simulation, and Test.” An early version of a general approach to verifying arithmetic circuits using polynomial representations.
R. E. Bryant, “A Switch-Level Model and Simulator for MOS Digital Systems,” IEEE Transactions on Computers, (February, 1984), pp. 160–177.

Describes the algorithmic basis for MOSSIM II, a logic simulator that models transistors as simple switches. This simulator and its successors were widely used in industry and academia in the 1980s. Intel used it to simulate several generations of microprocessor circuits.
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 was heavily used within Intel for many years.
R. E. Bryant, R. H. Katz, and E. D. Lazowska, “Bit-data Computing: Creating Revolutionary Breakthroughs in Commerce, Science, and Society,” Computing Community Consortium, 2008.

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

Professional Activities

Affiliations

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

Awards

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

Academic Review Committees

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

Conference Committees

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

Review Committees

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

Editorships and Reviewing

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

University Service

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

Publications

Books and Book Chapters

R. E. Bryant, “Binary Decision Diagrams: An Algorithmic Basis for Symbolic Model Checking” Handbook of Model Checking, E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds., Springer, 2018, pp. 191–218, Available as PDF.

R. E. Bryant, and D. R. O’Hallaron, Computer Systems: A Programmer’s Perspective, Third Edition, Prentice-Hall, 2015. More information available at CSAPP website

R. E. Bryant, and D. R. O’Hallaron, Computer Systems: A Programmer’s Perspective, Second Edition, Prentice-Hall, 2011.

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

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

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

R. E. Bryant, ed., Proceedings of the Third Caltech Conference on Very Large Scale Integration, Computer Science Press, March, 1983.

R. E. Bryant and J. B. Dennis, “Concurrent Programming,” in Research Directions in Software Technology, P. Wegner, ed., MIT Press, June, 1979, pp. 584–610. Revised version in Operating Systems Engineering, Lecture Notes in Computer Science 143, M. Maekawa and L. A. Belady, eds., Springer-Verlag, 1982, pp. 426–451. Electronic version available as PDF.

Refereed Journal and Book Articles

R. E. Bryant and M. J. H. Heule, “Generating Extended Resolution Proofs with a BDD-Based SAT Solver,” ACM Transactions on Computational Logic Volume 24, Number 4, 2023, pp. 1–28. Available as PDF. Also available as arXiv.

R. E. Bryant, “Chain Reduction for Binary and Zero-Suppressed Decision Diagrams,” Journal of Automated Reasoning, Vol. 64, No. 7 (2020), pp. 81–98. Available as PDF.

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

L. P. Huang, and R. E. Bryant, “Intractability in Linear Switch-Level Simulation,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 12, No. 6 (June, 1993), pp. 829–836.

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, PDF. Also available as PDF

S. A. Kravitz, R. E. Bryant, and R. A. Rutenbar, “Massively Parallel Switch-Level Simulation: A Feasibility Study,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 10, No. 7 (July, 1991) pp. 871–894.

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

D. L. Beatty, and R. E. Bryant, “Incremental Switch-Level Analysis,” IEEE Design and Test of Computers, Vol. 5, No. 6 (December, 1988), pp. 33–42.

R. E. Bryant, “A Survey of Switch-Level Algorithms,” IEEE Design and Test of Computers, Vol. 4, No. 4 (August, 1987), pp. 26–40.

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

W. J. Dally and R. E. Bryant, “A Hardware Architecture for Switch-Level Simulation,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. CAD-4, No. 3 (July, 1985), pp. 239–249.

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

R. E. Bryant, W. Nawrocki, J. Avigad, and M. J. H. Heule, “Certified Knowledge Compilation with Application to Formally Verified Model Counting,” Theory and Applications of Boolean Satifiability (SAT), July, 2023. Available as PDF.

R. E. Bryant, “TBUDDY: A Proof-Generating BDD Package,” Formal Methods in Computer-Aided Design FMCAD 2022, October, 2022. Available as PDF.

J. E. Reeves, R. E. Bryant, and M. J. H. Heule, “Preprocessing of Propagation Redundant Clauses,” International Joint Conference on Automated Reasoning IJCAR-2022, August, 2022. Available as PDF.

R. E. Bryant, A. Biere, and M. J. H. Heule, “Clausal Proofs for Pseudo-Boolean Reasoning,” Tools and Algorithms for the Construction and Analysis of Systems TACAS 2022, LNCS 12651, April, 2022. Available as PDF.

J. E. Reeves, M. J. H. Heule, and R. E. Bryant, “Moving Definition Variables in Quantified Boolean Formulas,” Tools and Algorithms for the Construction and Analysis of Systems TACAS 2022, LNCS 12651, April, 2022. Available as PDF.

R. E. Bryant and M. J. H. Heule, “Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver,” Computer-Aided Deduction CADE 2021, LNAI 12699, July, 2021, pp. 433–449. Available as PDF.

R. E. Bryant and M. J. H. Heule, “Generating Extended Resolution Proofs with a BDD-Based SAT Solver,” Tools and Algorithms for the Construction and Analysis of Systems TACAS 2021, LNCS 12651, April, 2021, pp. 76–93. Available as PDF. Extended version available on arXiv.

R. E. Bryant, “Chain Reduction for Binary and Zero-Suppressed Decision Diagrams,” Tools and Algorithms for the Construction and Analysis of Systems TACAS 2018, LNCS 10805, April, 2018, pp. 81–98. Available as PDF.

B. P. Railing, and R. E. Bryant, “Implementing Malloc: Students and Systems Programming,” 49th ACM Technical Symposium on Computer Science Education SIGCSE 2018, February, 2018. Available as PDF.

R. M. Fujimoto, R. Bagrodia, R. E. Bryant, K. M. Chandy, D. Jefferson, J. Misra, D. Nicol, and B. Unger, “Parallel Discrete Event Simulation: The Making of a Field,” Winter Simulation Conference 2017, December, 2017. Available as PDF

H. Cui, J. Šimša, 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. Šimša, 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 PDF

J. Šimša, 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 PDF. Expanded version available as Technical Report PDF.

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

R. E. Bryant, “Bit-Level Analysis of an SRT Divider Circuit,” 33rd Design Automation Conference, June, 1996, pp. 661–665. Available as 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 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 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 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 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 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 PDF.

T. J. Sheffler, and R. E. Bryant, “An Analysis of Hashing on Parallel and Vector Computers,” International Conference on Parallel Processing, August, 1993.

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

T. J. Sheffler, and R. E. Bryant, “Match and Move: an Approach to Data Parallel Computing,” MIT/Brown Conference on Advanced Research in VLSI and Parallel Systems, MIT Press, March, 1992, pp. 299–317.

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

D. L. Beatty, R. E. Bryant, and C.-J. H. Seger, “Synchronous Circuit Verification by Symbolic Simulation: An Illustration,” 6th MIT Conference on Advanced Research in VLSI and Parallel Systems, April, 1990, pp. 98–112.

C.-J. Seger, and R. E. Bryant, “Modeling of Circuit Delays in Symbolic Simulation,” IFIP Workshop on Applied Formal Methods for VLSI Design, November, 1989, pp. 625–639.

A. L. Fisher, and R. E. Bryant, “Performance of COSMOS on the IFIP Workshop Benchmarks,” IFIP Workshop on Applied Formal Methods for VLSI Design, November, 1989.

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

S. A. Kravitz, R. E. Bryant, and R. A. Rutenbar, “Massively Parallel Switch-Level Simulation—A Feasibility Study,” 26th Design Automation Conference, June, 1989, pp. 91–97.

S. A. Kravitz, R. E. Bryant, and R. A. Rutenbar, “Logic Simulation on Massively Parallel Architectures,” International Symposium on Computer Architecture, May, 1989, pp. 336–343.

R. E. Bryant, “Data Parallel Switch-Level Simulation,” IEEE International Conference on Computer-Aided Design, November, 1988, pp. 354–357. Available as PDF

D. Beatty and R. E. Bryant, “Fast Incremental Circuit Analyis Using Extracted Hierarchy,” 25th Design Automation Conference, June, 1988, pp. 495–500. Winner of the Best Paper Award, Design, Simulation and Test Category.

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

H. R. Sucar, P. Gelsinger, and R. E. Bryant, “Functional Test Grading as Applied to the 80386,” International Conference on Computer Design, IEEE, October, 1986, pp. 393–396.

R. E. Bryant and M. D. Schuster, “Performance Evaluation of FMOSSIM, a Concurrent, Switch-Level Fault Simulator,” 22nd Design Automation Conference, June, 1985, pp. 715–719.

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

W. J. Dally and R. E. Bryant, “A Special Purpose Processor for Switch-Level Simulation,” International Conference on Computer-Aided Design, IEEE, 1984.

M. D. Schuster and R. E. Bryant, “Concurrent Fault Simulation of MOS Digital Circuits,” Advanced Research in VLSI, P. Penfield, ed., Artech House, Dedham, MA., 1984, pp. 245–248. Reprinted in V. D. Agrawal and S. C. Seth, Test Generation for VLSI Chips, IEEE Computer Society Press, 1988, pp. 219–228.

R. E. Bryant, “Race Detection in MOS Circuits by Ternary Simulation,” VLSI 83, F. Anceau, ed., North-Holland, August, 1983, pp. 85–95.

R. E. Bryant, “A Switch-Level Model of MOS Logic Circuits,” VLSI 81, J. Gray, ed., Academic Press, August, 1981, pp. 329–340.

R. E. Bryant, “MOSSIM: A Switch-Level Simulator for MOS LSI,” 18th Design Automation Conference, July, 1981, pp. 786–790. Also in 25 Years of Electronic Design Automation, ACM/IEEE, 1988, pp. 426–430.

R. E. Bryant, “Simulation on a Distributed System,” First International Conference on Distributed Systems, IEEE, October, 1979, pp. 544–552. Electronic version available as PDF

Unrefereed Articles

M. Soos and R. E. Bryant “Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination,” Pragmatics of SAT Workshop, 2022. Available as PDF and arXiv

D. McDonald, D. Ackley, R. Bryant, M. Gedney, H. Hirsh, L. Shanley, “Antisocial Computing: Exploring Design Risks in Social Computing Systems,” ACM Interactions, Vol. 21, No. 6 (October, 2014), pp. 72–75, available as PDF.

R. E. Bryant, “A View from the Engine Room: Computational Support for Symbolic Model Checking,” 25 Years of Model Checking, H. Veith and O. Grunberg, eds. LNCS-4925, Springer-Verlag, 2007, available as 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 PDF, and Term Rewriting and Applications RTA 2006, LNCS 4098, Springer-Verlag, July, 2006, pp. 1–3, available as 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 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 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 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 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 PDF.

R. E. Bryant, “Formal Verification of Pipelined Processors,” Tools and Algorithms for the Construction and Analysis of Systems TACAS ’98, B. Steffen, ed., LNCS 1384, Springer-Verlag, March 1998, pp. 1–4.

R. E. Bryant, “Multipliers and Dividers: Insights on Arithmetic Circuit Verification,” Invited paper, Computer-Aided Verification CAV ’97, P. Wolper, Ed., LNCS 939, Springer-Verlag, 1995, pp. 1–3.

R. E. Bryant, “Symbolic Analysis Methods for Masks, Circuits, and Systems,” Invited paper, International Conference on Computer Design ICCD ’93, October, 1993. Available as PDF.

R. E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams,” Second Makuhari International Conference on High Technology, Chiba, Japan, 1990.

R. E. Bryant, “Formal Hardware Verification by Symbolic Simulation,” VLSI Logic Synthesis and Design, R. W. Dutton, ed., IOS Press, Amsterdam, 1991.

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

K. Cho, and R. E. Bryant, “Test Pattern Generation for Combinational and Sequential MOS Circuits by Symbolic Fault Simulation,” TECHCON-88, Semiconductor Research Corp., October, 1988.

S. A. Kravitz, and R. E. Bryant “Massively Parallel Logic Simulation,” TECHCON-88, Semiconductor Research Corp., October, 1988.

R. E. Bryant, “Compiled Simulation of MOS Circuits,” Canadian Conference on VLSI, October, 1986, pp. 217–219.

R. E. Bryant, “Can a Simulator Verify a Circuit?,” in Formal Aspects of VLSI Design, G. J. Milne, and P. A. Subrahmanyam, eds., North-Holland, 1986, pp. 125–136. Reprinted in M. Yoeli, Formal Verification of Hardware Design, IEEE Computer Society Press, 1990, pp. 272–281.

R. E. Bryant and M. D. Schuster, “Fault Simulation of MOS Digital Circuits,” VLSI Design, October, 1983, pp. 24–30.

R. E. Bryant, “Switch-Level Modeling of MOS Digital Circuits,” International Conference on Circuits and Systems, Rome, Italy, May, 1982, pp. 68–71.

R. E. Bryant, “An Algorithm for MOS Logic Simulation,” Lambda Magazine, Fourth Quarter, 1980, pp. 46–53.

Arvind, and R. E. Bryant, “Design Considerations for a Partial Differential Equation Machine,” Proceedings of the Scientific Computing Information Exchange Meeting, 1979.

Unpublished

R. E. Bryant, “Notes on ‘BDD-Based Bucket Elimination’,” 2023, Available on arXiv

R. E. Bryant, “Formal Verification of Pipelined Y86-64 Microprocessors with Uclid5,” Technical report CMU-CS-18-122. Available as PDF.

R. E. Bryant, K. Sutner, and M. J. Stehlik, “Introductory Computer Science Education at Carnegie Mellon University: A Deans’ Perspective,” Technical report CMU-CS-10-140. Available as PDF.

R. E. Bryant, “Data-Intensive Supercomputing: The Case for DISC,” Technical report CMU-CS-07-128. Available as PDF.

R. E. Bryant, “Term-Level Verification of a CISC Microprocessor,” Technical report CMU-CS-05-195. Available as 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 PDF.

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

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

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

D. Beatty, K. Brace, R. E. Bryant, K. Cho, and L. Huang, User’s Guide to COSMOS, 1987.

M. Schuster, and R. E. Bryant, FMOSSIM: A Switch-Level Logic and Fault Simulator, unpublished user’s manual, 1985.

R. E. Bryant, M. Schuster, and D. Whiting, MOSSIM II: A Switch-Level Simulator for MOS LSI, User’s Manual, Technical Report 5033, Caltech Computer Science, 1982. Available as 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 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 PDF.

Technical Presentations

Professional Meetings and Conferences

Invited talks indicated with asterisk.

4/5/22: “Clausal Proofs for Pseudo-Boolean Reasoning,” Tools and Algorithms for the Construction and Analysis of Systems, Munich, Germany.
7/14/21: “Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver,” Computer-Aided Deduction, Held online.
7/6/21: “Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver,” Workshop on Quantified Boolean Formulas, Held online.
4/29/21: “Generating Extended Resolution Proofs with a BDD-Based SAT Solver,” Tools and Algorithms for the Construction and Analysis of Systems, Held online.
4/17/18: “Chain Reduction for Binary and Zero-Suppressed Decision Diagrams,” Tools and Algorithms for the Construction and Analysis of Systems, Thessaloniki, Greece.
*5/23/16: “Creating Foundations for Parallel and Distributed Computing,” Keynote presentation, NSF/TCPP Workshop on Parallel and Distributed Computing Education, Chicago, IL
*4/29/16: “Moore’s Law: Another 50 Years?,” Symposium on Programming: Logics, Models, Algorithms and Concurrency, Austin, TX
*3/5/16: “Introducing Computer Systems from a Programmer’s Perspective,” Keynote presentation, Workshop on Connecting Concepts Across the Curriculum, Baton Rouge, LA
*11/18/15: “The National Strategic Computing Initiative,” International Conference for High Performance Computing, Networking, Storage and Analysis, Austin, TX
*11/18/15: “Supercomputing and Big Data: A Convergence?,” as part of a panel session on “Supercomputing and Big Data: From Collision to Convergence” at International Conference for High Performance Computing, Networking, Storage and Analysis, Austin, TX
*9/10/15: “The National Strategic Computing Initiative,” as part of a panel session at HPC User Forum, Broomfield, CO
*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

5/31–6/1/2022

“Trustworthy Boolean Reasoning,” Summer School on Formal Technologies, Menlo Park, CA.

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

Current: Joseph Reeves, CMU CS (jointly advised by Marijn Heule).
2013: Jiří Š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 at Aries Design Automation
2004: Shuvendu Lahiri, CMU ECE. Now at Microsoft Research.
2004: Amit Goel, CMU ECE. Now at Amazon.
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 Synopsys.
1993: Derek Beatty, CMU CS. Now at Synopsys.
1992: Karl Brace, CMU ECE. Now at Intel Corporation.
1992: Tom Sheffler, CMU ECE. Now at Roche Sequencing Solutions.
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 Caltech.
1998: Vishnu Patankar, CMU ECE. Now at Amazon.
1994: Samir Jain, CMU ECE.
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

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