Randal E. Bryant

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

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

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

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

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

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
`http://www.cs.cmu.edu/~bryant/pubdir/MIT-CSG-148-2.pdf`.

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

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

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

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

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

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

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

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

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

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

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

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

C.-J. H. Seger, and R. E. Bryant,
``Formal Verification by Symbolic
Evaluation of Partially-Ordered Trajectories,''
*Formal Methods in System Design*,
Vol. 6, No. 2 (March, 1995), pp. 147-190.
Preprint version available as
`http://www.cs.cmu.edu/~bryant/pubdir/fmsd95.pdf`.

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

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

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

R. E. Bryant,
``On the Complexity of VLSI Implementations and Graph Representations of
Boolean Functions with Application to Integer Multiplication,''
*IEEE Transactions on Computers*, Vol. 40, No. 2 (February, 1991),
pp. 205-213.
Preprint available as
`http://www.cs.cmu.edu/~bryant/pubdir/ieeetc91.pdf`.

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

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

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

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

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

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*,
April, 2022. Available as
`http://www.cs.cmu.edu/~bryant/pubdir/tacas22-rhb.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
`http://www.cs.cmu.edu/~bryant/pubdir/cade21.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
`http://www.cs.cmu.edu/~bryant/pubdir/tacas21.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
`http://www.cs.cmu.edu/~bryant/pubdir/tacas18.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
`http://www.cs.cmu.edu/~bryant/pubdir/sigcse18.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
`http://www.cs.cmu.edu/~bryant/pubdir/wsc17.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
`http://www.cs.cmu.edu/~bryant/pubdir/fmcad11.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
`http://www.cs.cmu.edu/~bryant/pubdir/memocode10.pdf`.

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

M. Christodorescu, S. Jha, S. A. Seshia, D. Song, and R. E. Bryant,
``Semantics Aware Malware Detection,''
*IEEE Symposium on Security and Privacy*,
May, 2005,
pp. 32-46.
Available as
`http://www.cs.cmu.edu/~bryant/pubdir/oakland05.pdf`.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

K. S. Brace, R. L. Rudell, and R. E. Bryant, ``Efficient
Implementation of a BDD Package,'' *27th Design Automation
Conference*, June, 1990, pp. 40-45.
For those who subscribe to the IEEE Xplore publication service, you
can get an electronic copy from
`http://ieeexplore.ieee.org/iel2/790/3382/00114826.pdf?isNumber=3382`.

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

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

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

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

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

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

R. E. Bryant,
``Simulation on a Distributed System,'' *First International Conference
on Distributed Systems*, IEEE, October, 1979, pp. 544-552.
Electronic version available as
`http://www.cs.cmu.edu/~bryant/pubdir/MIT-CSG-182.pdf`

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Randal E Bryant 2022-01-27