Randal E. Bryant
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.
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.
J. E. Reeves, M. J. H. Heule, and R. E. Bryant, “From Clauses to Klauses,” Computer-Aided Verification, LNCS 14681, July, 2024. Available as PDF.
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
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.
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.