Randal E. Bryant

168 papers A* 51A 21B 11C 6Misc 2Journal 51Unranked 24

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Certified Knowledge Compilation with Application to Formally Verified Model Counting. CoRR Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
2025	J	`jnl`	Certified Knowledge Compilation with Application to Formally Verified Model Counting. J. Artif. Intell. Res. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
2025	A	`conf`	Certifying Projected Knowledge Compilation. SAT Randal E. Bryant, Yong Kiam Tan, Marijn J. H. Heule
2025	J	`jnl`	Numerical Considerations in Weighted Model Counting. CoRR Randal E. Bryant
2024	—	`conf`	From Clauses to Klauses. CAV (1) Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
2024	B	`conf`	Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs. FMCAD Karthik V. Nukala, Soumyaditya Choudhuri, Randal E. Bryant, Marijn J. H. Heule
2023	A	`conf`	Certified Knowledge Compilation with Application to Verified Model Counting. SAT Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
2023	J	`jnl`	Generating Extended Resolution Proofs with a BDD-Based SAT Solver. ACM Trans. Comput. Log. Randal E. Bryant, Marijn J. H. Heule
2023	J	`jnl`	Notes on "Bounds on BDD-Based Bucket Elimination". CoRR Randal E. Bryant
2023	J	`jnl`	Preprocessing of Propagation Redundant Clauses. J. Autom. Reason. Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
2023	J	`jnl`	Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination. CoRR Mate Soos, Randal E. Bryant
2022	—	`conf`	Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) Randal E. Bryant, Armin Biere, Marijn J. H. Heule
2022	—	`conf`	Moving Definition Variables in Quantified Boolean Formulas. TACAS (1) Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
2022	A	`conf`	Preprocessing of Propagation Redundant Clauses. IJCAR Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
2022	B	`conf`	Tbuddy: A Proof-Generating BDD Package. FMCAD Randal E. Bryant
2021	A	`conf`	Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. CADE Randal E. Bryant, Marijn J. H. Heule
2021	—	`conf`	Generating Extended Resolution Proofs with a BDD-Based SAT Solver. TACAS (1) Randal E. Bryant, Marijn J. H. Heule
2021	J	`jnl`	Generating Extended Resolution Proofs with a BDD-Based SAT Solver. CoRR Randal E. Bryant, Marijn J. H. Heule
2020	J	`jnl`	Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. J. Autom. Reason. Randal E. Bryant
2020	J	`jnl`	From Data to Knowledge to Action: Enabling the Smart Grid. CoRR Randal E. Bryant, Randy H. Katz, Chase Hensel, Erwin P. Gianchandani
2020	J	`jnl`	Nonsilicon, Non-von Neumann Computing - Part II. Proc. IEEE Sankar Basu, Randal E. Bryant, Giovanni De Micheli, Thomas N. Theis, Lloyd Whitman
2019	J	`jnl`	Nonsilicon, Non-von Neumann Computing - Part I [Scanning the Issue]. Proc. IEEE Sankar Basu, Randal E. Bryant, Giovanni De Micheli, Thomas N. Theis, Lloyd Whitman
2018	—	`ch.`	Binary Decision Diagrams. Handbook of Model Checking Randal E. Bryant
2018	—	`conf`	Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. TACAS (1) Randal E. Bryant
2018	A	`conf`	Implementing Malloc: Students and Systems Programming. SIGCSE Brian P. Railing, Randal E. Bryant
2017	J	`jnl`	Advances in Artificial Intelligence Require Progress Across all of Computer Science. CoRR Gregory D. Hager, Randal E. Bryant, Eric Horvitz, Maja J. Mataric, Vasant G. Honavar
2017	J	`jnl`	Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. CoRR Randal E. Bryant
2017	Misc	`conf`	Parallel discrete event simulation: The making of a field. WSC Richard M. Fujimoto, Rajive L. Bagrodia, Randal E. Bryant, K. Mani Chandy, David R. Jefferson, Jayadev Misra, David M. Nicol, Brian W. Unger
2016	—	`conf`	EduPar 2016 Keynote. IPDPS Workshops Randal E. Bryant
2014	J	`jnl`	Antisocial computing: exploring design risks in social computing systems. Interactions David W. McDonald, David H. Ackley, Randal E. Bryant, Melissa Gedney, Haym Hirsh, Lea Shanley
2013	A*	`conf`	Parrot: a practical runtime for deterministic, stable, and reliable threads. SOSP Heming Cui, Jirí Simsa, Yi-Hong Lin, Hao Li, Ben Blum, Xinan Xu, Junfeng Yang, Garth A. Gibson, Randal E. Bryant
2011	J	`jnl`	Data-Intensive Scalable Computing for Scientific Applications. Comput. Sci. Eng. Randal E. Bryant
2011	B	`conf`	Learning conditional abstractions. FMCAD Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia
2010	J	`jnl`	2009 CAV award announcement. Formal Methods Syst. Des. Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi
2010	C	`conf`	ATLAS: Automatic Term-level abstraction of RTL designs. MEMOCODE Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, John W. O'Leary
2009	J	`jnl`	An abstraction-based decision procedure for bit-vector arithmetic. Int. J. Softw. Tools Technol. Transf. Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
2009	J	`jnl`	The 2008 CAV Award citation. Formal Methods Syst. Des. Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi
2008	—	`conf`	A View from the Engine Room: Computational Support for Symbolic Model Checking. 25 Years of Model Checking Randal E. Bryant
2008	J	`jnl`	State-set branching: Leveraging BDDs for heuristic search. Artif. Intell. Rune Møller Jensen, Manuela M. Veloso, Randal E. Bryant
2007	A	`conf`	Deciding Bit-Vector Arithmetic with Abstraction. TACAS Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
2007	J	`jnl`	On Solving Boolean Combinations of UTVPI Constraints. J. Satisf. Boolean Model. Comput. Sanjit A. Seshia, K. Subramani, Randal E. Bryant
2007	J	`jnl`	Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. Shuvendu K. Lahiri, Randal E. Bryant
2006	A*	`conf`	Formal Verification of Infinite State Systems Using Boolean Methods. LICS Randal E. Bryant
2006	—	`conf`	Formal Verification of Infinite State Systems Using Boolean Methods. RTA Randal E. Bryant
2005	A*	`conf`	Automatic discovery of API-level exploits. ICSE Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant
2005	J	`jnl`	Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds CoRR Sanjit A. Seshia, Randal E. Bryant
2005	J	`jnl`	Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. Log. Methods Comput. Sci. Sanjit A. Seshia, Randal E. Bryant
2005	A	`conf`	Decision Procedures Customized for Formal Verification. CADE Randal E. Bryant, Sanjit A. Seshia
2005	—	`conf`	Modeling and Verifying Circuits Using Generalized Relative Timing. ASYNC Sanjit A. Seshia, Randal E. Bryant, Kenneth S. Stevens
2005	—	`conf`	Semantics-Aware Malware Detection. S&P Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Xiaodong Song, Randal E. Bryant
2005	J	`jnl`	TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories. Int. J. Embed. Syst. Miroslav N. Velev, Randal E. Bryant
2004	B	`conf`	Constructing Quantified Invariants via Predicate Abstraction. VMCAI Shuvendu K. Lahiri, Randal E. Bryant
2004	A*	`conf`	Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. LICS Sanjit A. Seshia, Randal E. Bryant
2004	A*	`conf`	Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic Non-Deterministic Planning. ICAPS Rune Møller Jensen, Manuela M. Veloso, Randal E. Bryant
2004	A*	`conf`	Indexed Predicate Discovery for Unbounded System Verification. CAV Shuvendu K. Lahiri, Randal E. Bryant
2004	J	`jnl`	Predicate Abstraction with Indexed Predicates CoRR Shuvendu K. Lahiri, Randal E. Bryant
2004	A	`conf`	Revisiting Positive Equality. TACAS Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur
2004	A*	`conf`	Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. CAV Amit Goel, Randal E. Bryant
2004	C	`conf`	System modeling and verification with UCLID. MEMOCODE Randal E. Bryant
2004	A	`conf`	Verifying properties of hardware and software by predicate abstraction and model checking. ICCAD Randal E. Bryant, Sriram K. Rajamani
2003	A*	`conf`	A Symbolic Approach to Predicate Abstraction. CAV Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook
2003	A*	`conf`	A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. DAC Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant
2003	—	`book`	Computer systems - a programmers perspective. Randal E. Bryant, David R. O'Hallaron
2003	—	`conf`	Convergence Testing in Term-Level Bounded Model Checking. CHARME Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
2003	A*	`conf`	Deductive Verification of Advanced Out-of-Order Microprocessors. CAV Shuvendu K. Lahiri, Randal E. Bryant
2003	J	`jnl`	Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. Miroslav N. Velev, Randal E. Bryant
2003	A*	`conf`	Guided Symbolic Universal Planning. ICAPS Rune Møller Jensen, Manuela M. Veloso, Randal E. Bryant
2003	—	`conf`	Reasoning about Infinite State Systems Using Boolean Methods. FSTTCS Randal E. Bryant
2003	A	`conf`	Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis. DATE Amit Goel, Randal E. Bryant
2003	A*	`conf`	Symbolic representation with ordered function templates. DAC Amit Goel, Gagan Hasteer, Randal E. Bryant
2003	A*	`conf`	Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. CAV Sanjit A. Seshia, Randal E. Bryant
2002	J	`jnl`	Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. Randal E. Bryant, Miroslav N. Velev
2002	A*	`conf`	Deciding Separation Formulas with SAT. CAV Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant
2002	B	`conf`	Modeling and Verification of Out-of-Order Microprocessors in UCLID. FMCAD Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant
2002	A*	`conf`	Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. CAV Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
2002	J	`jnl`	Ordered Binary Decision Diagrams in Electronic Design Automation Universität Trier, Mathematik/Informatik, Forschungsbericht Randal E. Bryant, Christoph Meinel
2002	—	`conf`	SetA*: An Efficient BDD-Based Heuristic Search Algorithm. AAAI/IAAI Rune Møller Jensen, Randal E. Bryant, Manuela M. Veloso
2001	A	`conf`	A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells. ICCAD Clayton B. McDonald, Randal E. Bryant
2001	J	`jnl`	An efficient graph representation for arithmetic circuitverification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Yirng-An Chen, Randal E. Bryant
2001	J	`jnl`	CMOS circuit verification with symbolic switch-level timingsimulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Clayton B. McDonald, Randal E. Bryant
2001	A*	`conf`	Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis. DAC Clayton B. McDonald, Randal E. Bryant
2001	A*	`conf`	EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. CAV Miroslav N. Velev, Randal E. Bryant
2001	A*	`conf`	Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. DAC Miroslav N. Velev, Randal E. Bryant
2001	A	`conf`	Introducing computer systems from a programmer's perspective. SIGCSE Randal E. Bryant, David R. O'Hallaron
2001	J	`jnl`	Limitations and challenges of computer-aided design technology for CMOS VLSI. Proc. IEEE Randal E. Bryant, Kwang-Ting Cheng, Andrew B. Kahng, Kurt Keutzer, Wojciech Maly, A. Richard Newton, Lawrence T. Pileggi, Jan M. Rabaey, Alberto L. Sangiovanni-Vincentelli
2001	J	`jnl`	Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Log. Randal E. Bryant, Steven M. German, Miroslav N. Velev
2001	J	`jnl`	Verification of arithmetic circuits using binary moment diagrams. Int. J. Softw. Tools Technol. Transf. Randal E. Bryant, Yirng-An Chen
2000	B	`conf`	A Theory of Consistency for Modular Synchronous Systems. FMCAD Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel
2000	J	`jnl`	Boolean Satisfiability with Transitivity Constraints CoRR Randal E. Bryant, Miroslav N. Velev
2000	A*	`conf`	Boolean Satisfiability with Transitivity Constraints. CAV Randal E. Bryant, Miroslav N. Velev
2000	A*	`conf`	Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. DAC Miroslav N. Velev, Randal E. Bryant
2000	B	`conf`	Symbolic Simulation with Approximate Values. FMCAD Chris Wilson, David L. Dill, Randal E. Bryant
2000	A*	`conf`	Symbolic timing simulation using cluster scheduling. DAC Clayton B. McDonald, Randal E. Bryant
1999	A*	`conf`	Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. DAC Miroslav N. Velev, Randal E. Bryant
1999	A*	`conf`	Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. CAV Randal E. Bryant, Steven M. German, Miroslav N. Velev
1999	J	`jnl`	Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Manish Pandey, Randal E. Bryant
1999	Misc	`conf`	Formal Verification of an ARM Processor. VLSI Design Vishnu A. Patankar, Alok Jain, Randal E. Bryant
1999	B	`conf`	Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. TABLEAUX Randal E. Bryant, Steven M. German, Miroslav N. Velev
1999	A*	`conf`	Optimizing Symbolic Model Checking for Constraint-Rich Models. CAV Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron
1999	J	`jnl`	Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic CoRR Randal E. Bryant, Steven M. German, Miroslav N. Velev
1999	—	`conf`	Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. CHARME Miroslav N. Velev, Randal E. Bryant
1999	A	`conf`	Symbolic functional and timing verification of transistor-level circuits. ICCAD Clayton B. McDonald, Randal E. Bryant
1998	B	`conf`	A Performance Study of BDD-Based Model Checking. FMCAD Bwolen Yang, Randal E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, Fabio Somenzi
1998	B	`conf`	Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. FMCAD Miroslav N. Velev, Randal E. Bryant
1998	A	`conf`	Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. TACAS Miroslav N. Velev, Randal E. Bryant
1998	A	`conf`	Formal Verification of Pipelined Processors. TACAS Randal E. Bryant
1998	C	`conf`	Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. ICCD Miroslav N. Velev, Randal E. Bryant
1998	A*	`ed.`	Proceedings of the 35th Conference on Design Automation, Moscone center, San Francico, California, USA, June 15-19, 1998. DAC Basant R. Chawla, Randal E. Bryant, Jan M. Rabaey
1998	—	`conf`	Space- and Time-Efficient BDD Construction via Working Set Control. ASP-DAC Bwolen Yang, Yirng-An Chen, Randal E. Bryant, David R. O'Hallaron
1998	A*	`conf`	User Experience with High Level Formal Verification (Panel). DAC Randal E. Bryant, Gerry Musgrave
1998	A*	`conf`	Verification of Floating-Point Adders. CAV Yirng-An Chen, Randal E. Bryant
1998	—	`conf`	Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. ACSD Miroslav N. Velev, Randal E. Bryant
1997	A*	`conf`	Efficient Modeling of Memory Arrays in Symbolic Simulation. CAV Miroslav N. Velev, Randal E. Bryant, Alok Jain
1997	A*	`conf`	Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. CAV Manish Pandey, Randal E. Bryant
1997	A*	`conf`	Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation. DAC Manish Pandey, Richard Raimi, Randal E. Bryant, Magdy S. Abadir
1997	A*	`conf`	Formal Verification of a Superscalar Execution Unit. DAC Kyle L. Nelson, Alok Jain, Randal E. Bryant
1997	A	`conf`	PHDD: an efficient graph representation for floating point circuit verification. ICCAD Yirng-An Chen, Randal E. Bryant
1997	—	`conf`	Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. ASIAN Randal E. Bryant, Miroslav N. Velev
1996	A	`conf`	ACV: an arithmetic circuit verifier. ICCAD Yirng-An Chen, Randal E. Bryant
1996	A*	`conf`	Bit-Level Analysis of an SRT Divider Circuit. DAC Randal E. Bryant
1996	A*	`conf`	Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation. DAC Manish Pandey, Richard Raimi, Derek L. Beatty, Randal E. Bryant
1996	B	`conf`	Verifying Nondeterministic Implementations of Deterministic Systems. FMCAD Alok Jain, Kyle L. Nelson, Randal E. Bryant
1995	A*	`conf`	Automatic Clock Abstraction from Sequential Circuits. DAC Samir Jain, Randal E. Bryant, Alok Jain
1995	A	`conf`	Binary decision diagrams and beyond: enabling technologies for formal verification. ICCAD Randal E. Bryant
1995	C	`conf`	Extraction of finite state machines from transistor netlists by symbolic simulation. ICCD Manish Pandey, Alok Jain, Randal E. Bryant, Derek L. Beatty, Gary York, Samir Jain
1995	J	`jnl`	Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Formal Methods Syst. Des. Carl-Johan H. Seger, Randal E. Bryant
1995	A*	`conf`	Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract). CAV Randal E. Bryant
1995	A*	`conf`	Verification of Arithmetic Circuits with Binary Moment Diagrams. DAC Randal E. Bryant, Yirng-An Chen
1994	—	`conf`	Digital Circuit Verification Using Partially-Ordered State Models. ISMVL Carl-Johan H. Seger, Randal E. Bryant
1994	A*	`conf`	Formally Verifying a Microprocessor Using a Simulation Methodology. DAC Derek L. Beatty, Randal E. Bryant
1993	—	`conf`	An Analysis of Hashing on Parallel and Vector Computers. ICPP (3) Thomas J. Sheffler, Randal E. Bryant
1993	C	`conf`	Geometric characterization of series-parallel variable resistor networks. ISCAS Randal E. Bryant, J. D. Tygar, Lawrence P. Huang
1993	J	`jnl`	Intractability in linear switch-level simulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Lawrence P. Huang, Randal E. Bryant
1993	A	`conf`	Inverter minimization in multi-level logic networks. ICCAD Alok Jain, Randal E. Bryant
1993	C	`conf`	Symbolic Analysis Methods for Masks, Circuits, and Systems. ICCD Randal E. Bryant
1992	—	`conf`	Formal Verification: A Slow, but Certain Evolution. IFIP Congress (1) Randal E. Bryant
1992	J	`jnl`	Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Comput. Surv. Randal E. Bryant
1991	J	`jnl`	A Methodology for Hardware Verification Based on Logic Simulation. J. ACM Randal E. Bryant
1991	A	`conf`	Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis. ICCAD Randal E. Bryant
1991	A*	`conf`	Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation. DAC Randal E. Bryant, Derek L. Beatty, Carl-Johan H. Seger
1991	J	`jnl`	Formal verification of memory circuits by switch-level simulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Randal E. Bryant
1991	A*	`conf`	Mapping Switch-Level Simulation onto Gate-Level Hardware Accelerators. DAC Alok Jain, Randal E. Bryant
1991	J	`jnl`	Massively parallel switch-level simulation: a feasibility study. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar
1991	J	`jnl`	On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication. IEEE Trans. Computers Randal E. Bryant
1990	A*	`conf`	Efficient Implementation of a BDD Package. DAC Karl S. Brace, Richard L. Rudell, Randal E. Bryant
1990	A*	`conf`	Formal Verification of Digital Circuits Using Symbolic Ternary System Models. CAV Randal E. Bryant, Carl-Johan H. Seger
1990	—	`conf`	Formal Verification of Digital Circuits Using Symbolic Ternary System Models. CAV (DIMACS/AMS volume) Randal E. Bryant, Carl-Johan H. Seger
1990	A*	`conf`	Symbolic Simulation - Techniques and Applications. DAC Randal E. Bryant
1989	A*	`conf`	Logic Simulation on Massively Parallel Architectures. ISCA Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar
1989	A*	`conf`	Massively Parallel Switch-Level Simulation: A Feasibility Study. DAC Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar
1989	—	`conf`	Silicon Compilers: How Well Have They Done, and Where Are They Headed? IFIP Congress Randal E. Bryant
1989	A*	`conf`	Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation. DAC Kyeongsoon Cho, Randal E. Bryant
1989	—	`conf`	Verification of Synchronous Circuits by Symbolic Logic Simulation. Hardware Specification, Verification and Synthesis Randal E. Bryant
1988	A*	`conf`	CAD Tool Needs for System Designers. DAC Randal E. Bryant
1988	A	`conf`	Data parallel switch-level simulation. ICCAD Randal E. Bryant
1988	A*	`conf`	Fast Incremental Circuit Analysis Using Extracted Hierarchy. DAC Derek L. Beatty, Randal E. Bryant
1988	J	`jnl`	Incremental switch-level analysis. IEEE Des. Test Derek L. Beatty, Randal E. Bryant
1987	J	`jnl`	A Survey of Switch-Level Algorithms. IEEE Des. Test Randal E. Bryant
1987	J	`jnl`	Algorithmic Aspects of Symbolic Switch Network Analysis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Randal E. Bryant
1987	J	`jnl`	Boolean Analysis of MOS Circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Randal E. Bryant
1987	A*	`conf`	COSMOS: A Compiled Simulator for MOS Circuits. DAC Randal E. Bryant, Derek L. Beatty, Karl S. Brace, Kyeongsoon Cho, Thomas J. Sheffler
1986	J	`jnl`	Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers Randal E. Bryant
1985	J	`jnl`	A Hardware Architecture for Switch-Level Simulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. William J. Dally, Randal E. Bryant
1985	A*	`conf`	Performance evaluation of FMOSSIM, a concurrent switch-level fault simulator. DAC Randal E. Bryant, Michael Dd. Schuster
1985	A*	`conf`	Symbolic manipulation of Boolean functions using a graphical representation. DAC Randal E. Bryant
1984	J	`jnl`	A Switch-Level Model and Simulator for MOS Digital Systems. IEEE Trans. Computers Randal E. Bryant
1981	A*	`conf`	MOSSIM: A switch-level simulator for MOS LSI. DAC Randal E. Bryant
1980	—	`conf`	Concurrent programming. Operating Systems Engineering Randal E. Bryant, Jack B. Dennis