next_inactive up previous


Randal E. Bryant

Partial List of Publications

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

Books and Book Chapters

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

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

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

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

Refereed Journal and Book Articles

R. E. Bryant, ``Data-Intensive Scalable Computing for Scientific Applications,'' IEEE Computing in Science and Engineering, Vol. 13, No. 6 (2011), pp. 25-33.

R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady, ``An Abstraction-Based Decision Procedure for Bit-Vector Arithmetic,'' International Journal of Software Tools for Technology, Springer-Verlag Vol. 11, No. 2 (April, 2009), pp. 95-104.

R. M. Jensen, M. M. Veloso, and R. E. Bryant, ``State-Set Branching: Leveraging BDDs for Heuristic Search,'' Artificial Intelligence, Vol. 172, Issues 2-3 (February, 2008), pp. 103-139. Available as
http://www.cs.cmu.edu/~bryant/pubdir/aij07.pdf.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Refereed Conference Articles

H. Cui, J. Simsa, Y.-H. Ling, H. Li, B. Blum, X. Xu, J. Yang, G. A. Gibson, and R. E. Bryant, ``PARROT: A Practical Runtime for Deterministic, Stable, and Reliable Threads,'' 24th ACM Symposium on Operating Systems Principles, 2013.

J. Simsa, R. Bryant, G. A. Gibson, and J. Hickey, ``Scalable Dynamic Partial Order Reduction,'' 3rd International Conference on Runtime Verification, 2012.

B. A. Brady, R. E. Bryant, and S. A. Seshia, ``Learning Conditional Abstractions,'' Formal Methods in Computer-Aided Design, October, 2011, pp. 116-124. Available as
http://www.cs.cmu.edu/~bryant/pubdir/fmcad11.pdf

B. A. Brady, R. E. Bryant, S. A. Seshia, and J. W. O'Leary, ``ATLAS: Automatic Term-Level Abstraction of RTL Designs,'' Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July, 2010. Available as
http://www.cs.cmu.edu/~bryant/pubdir/memocode10.pdf.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Unrefereed Articles

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

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

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

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

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

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

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

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

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

Unpublished

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

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

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

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

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

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

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

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

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

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


next_inactive up previous
Randal E Bryant 2014-07-01