Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDRandal E. Bryant
Person information
- affiliation: Carnegie Mellon University, Pittsburgh, USA
- award (2007): IEEE Emanuel R. Piore Award
- award (1998): Paris Kanellakis Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
Books and Theses
- 2003
[b1]Randal E. Bryant, David R. O'Hallaron:
Computer systems - a programmers perspective. Pearson Education 2003, ISBN 978-0-13-178456-7, pp. I-XXVIII, 1-978
Journal Articles
- 2023
- [j37]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Preprocessing of Propagation Redundant Clauses. J. Autom. Reason. 67(3): 31 (2023) - [j36]Randal E. Bryant
, Marijn J. H. Heule:
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. ACM Trans. Comput. Log. 24(4): 31:1-31:28 (2023) - 2020
- [j35]Randal E. Bryant:
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. J. Autom. Reason. 64(7): 1361-1391 (2020) - [j34]Sankar Basu, Randal E. Bryant, Giovanni De Micheli, Thomas N. Theis, Lloyd Whitman:
Nonsilicon, Non-von Neumann Computing - Part II. Proc. IEEE 108(8): 1211-1218 (2020) - 2019
- [j33]Sankar Basu, Randal E. Bryant, Giovanni De Micheli, Thomas N. Theis, Lloyd Whitman:
Nonsilicon, Non-von Neumann Computing - Part I [Scanning the Issue]. Proc. IEEE 107(1): 11-18 (2019) - 2014
- [j32]David W. McDonald, David H. Ackley, Randal E. Bryant, Melissa Gedney, Haym Hirsh, Lea Shanley:
Antisocial computing: exploring design risks in social computing systems. Interactions 21(6): 72-75 (2014) - 2011
- [j31]Randal E. Bryant:
Data-Intensive Scalable Computing for Scientific Applications. Comput. Sci. Eng. 13(6): 25-33 (2011) - 2010
- [j30]Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi:
2009 CAV award announcement. Formal Methods Syst. Des. 36(3): 195-197 (2010) - 2009
- [j29]Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi:
The 2008 CAV Award citation. Formal Methods Syst. Des. 35(1): 4-5 (2009) - [j28]Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady:
An abstraction-based decision procedure for bit-vector arithmetic. Int. J. Softw. Tools Technol. Transf. 11(2): 95-104 (2009) - 2008
- [j27]Rune Møller Jensen, Manuela M. Veloso, Randal E. Bryant:
State-set branching: Leveraging BDDs for heuristic search. Artif. Intell. 172(2-3): 103-139 (2008) - 2007
- [j26]Sanjit A. Seshia, K. Subramani, Randal E. Bryant:
On Solving Boolean Combinations of UTVPI Constraints. J. Satisf. Boolean Model. Comput. 3(1-2): 67-90 (2007) - [j25]Shuvendu K. Lahiri, Randal E. Bryant:
Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. 9(1): 4 (2007) - 2005
- [j24]Miroslav N. Velev, Randal 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. Int. J. Embed. Syst. 1(1/2): 134-149 (2005) - [j23]Sanjit A. Seshia, Randal E. Bryant:
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. Log. Methods Comput. Sci. 1(2) (2005) - 2003
- [j22]Miroslav N. Velev, Randal E. Bryant:
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. 35(2): 73-106 (2003) - 2002
- [j21]Randal E. Bryant, Miroslav N. Velev:
Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3(4): 604-627 (2002) - 2001
- [j20]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:
Limitations and challenges of computer-aided design technology for CMOS VLSI. Proc. IEEE 89(3): 341-365 (2001) - [j19]Randal E. Bryant, Yirng-An Chen:
Verification of arithmetic circuits using binary moment diagrams. Int. J. Softw. Tools Technol. Transf. 3(2): 137-155 (2001) - [j18]Clayton B. McDonald, Randal E. Bryant:
CMOS circuit verification with symbolic switch-level timingsimulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20(3): 458-474 (2001) - [j17]Yirng-An Chen, Randal E. Bryant:
An efficient graph representation for arithmetic circuitverification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20(12): 1443-1454 (2001) - [j16]Randal E. Bryant, Steven M. German, Miroslav N. Velev:
Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Log. 2(1): 93-134 (2001) - 1999
- [j15]Manish Pandey, Randal E. Bryant:
Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 18(7): 918-935 (1999) - 1995
- [j14]Carl-Johan H. Seger, Randal E. Bryant:
Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Formal Methods Syst. Des. 6(2): 147-189 (1995) - 1993
- [j13]Lawrence P. Huang, Randal E. Bryant:
Intractability in linear switch-level simulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 12(6): 829-836 (1993) - 1992
- [j12]Randal E. Bryant:
Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Comput. Surv. 24(3): 293-318 (1992) - 1991
- [j11]Randal E. Bryant:
A Methodology for Hardware Verification Based on Logic Simulation. J. ACM 38(2): 299-328 (1991) - [j10]Randal E. Bryant:
On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication. IEEE Trans. Computers 40(2): 205-213 (1991) - [j9]Randal E. Bryant:
Formal verification of memory circuits by switch-level simulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 10(1): 94-102 (1991) - [j8]Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar:
Massively parallel switch-level simulation: a feasibility study. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 10(7): 871-894 (1991) - 1988
- [j7]Derek L. Beatty, Randal E. Bryant:
Incremental switch-level analysis. IEEE Des. Test 5(6): 33-42 (1988) - 1987
- [j6]Randal E. Bryant:
A Survey of Switch-Level Algorithms. IEEE Des. Test 4(4): 26-40 (1987) - [j5]Randal E. Bryant:
Algorithmic Aspects of Symbolic Switch Network Analysis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 6(4): 618-633 (1987) - [j4]Randal E. Bryant:
Boolean Analysis of MOS Circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 6(4): 634-649 (1987) - 1986
- [j3]Randal E. Bryant:
Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8): 677-691 (1986) - 1985
- [j2]William J. Dally, Randal E. Bryant:
A Hardware Architecture for Switch-Level Simulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 4(3): 239-250 (1985) - 1984
- [j1]Randal E. Bryant:
A Switch-Level Model and Simulator for MOS Digital Systems. IEEE Trans. Computers 33(2): 160-177 (1984)
Conference and Workshop Papers
- 2023
- [c111]Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule:
Certified Knowledge Compilation with Application to Verified Model Counting. SAT 2023: 6:1-6:20 - 2022
- [c110]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Preprocessing of Propagation Redundant Clauses. IJCAR 2022: 106-124 - [c109]Randal E. Bryant:
Tbuddy: A Proof-Generating BDD Package. FMCAD 2022: 49-58 - [c108]Randal E. Bryant, Armin Biere, Marijn J. H. Heule:
Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) 2022: 443-461 - [c107]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Moving Definition Variables in Quantified Boolean Formulas. TACAS (1) 2022: 462-479 - 2021
- [c106]Randal E. Bryant, Marijn J. H. Heule:
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. CADE 2021: 433-449 - [c105]Randal E. Bryant, Marijn J. H. Heule:
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. TACAS (1) 2021: 76-93 - 2018
- [c104]Brian P. Railing, Randal E. Bryant:
Implementing Malloc: Students and Systems Programming. SIGCSE 2018: 104-109 - [c103]Randal E. Bryant:
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. TACAS (1) 2018: 81-98 - 2017
- [c102]Richard M. Fujimoto, Rajive L. Bagrodia, Randal E. Bryant, K. Mani Chandy, David R. Jefferson, Jayadev Misra, David M. Nicol, Brian W. Unger:
Parallel discrete event simulation: The making of a field. WSC 2017: 262-291 - 2016
- [c101]Randal E. Bryant:
EduPar 2016 Keynote. IPDPS Workshops 2016: 941 - 2013
- [c100]Heming Cui, Jirí Simsa, Yi-Hong Lin, Hao Li, Ben Blum, Xinan Xu, Junfeng Yang, Garth A. Gibson, Randal E. Bryant:
Parrot: a practical runtime for deterministic, stable, and reliable threads. SOSP 2013: 388-405 - 2011
- [c99]Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia:
Learning conditional abstractions. FMCAD 2011: 116-124 - 2010
- [c98]Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, John W. O'Leary:
ATLAS: Automatic Term-level abstraction of RTL designs. MEMOCODE 2010: 31-40 - 2008
- [c97]Randal E. Bryant:
A View from the Engine Room: Computational Support for Symbolic Model Checking. 25 Years of Model Checking 2008: 145-149 - 2007
- [c96]Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady:
Deciding Bit-Vector Arithmetic with Abstraction. TACAS 2007: 358-372 - 2006
- [c95]Randal E. Bryant:
Formal Verification of Infinite State Systems Using Boolean Methods. LICS 2006: 3-4 - [c94]Randal E. Bryant:
Formal Verification of Infinite State Systems Using Boolean Methods. RTA 2006: 1-3 - 2005
- [c93]Sanjit A. Seshia, Randal E. Bryant, Kenneth S. Stevens:
Modeling and Verifying Circuits Using Generalized Relative Timing. ASYNC 2005: 98-108 - [c92]Randal E. Bryant, Sanjit A. Seshia:
Decision Procedures Customized for Formal Verification. CADE 2005: 255-259 - [c91]Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant:
Automatic discovery of API-level exploits. ICSE 2005: 312-321 - [c90]Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Xiaodong Song, Randal E. Bryant:
Semantics-Aware Malware Detection. S&P 2005: 32-46 - 2004
- [c89]Rune Møller Jensen, Manuela M. Veloso, Randal E. Bryant:
Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic Non-Deterministic Planning. ICAPS 2004: 335-344 - [c88]Shuvendu K. Lahiri, Randal E. Bryant:
Indexed Predicate Discovery for Unbounded System Verification. CAV 2004: 135-147 - [c87]Amit Goel, Randal E. Bryant:
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. CAV 2004: 255-267 - [c86]Randal E. Bryant, Sriram K. Rajamani:
Verifying properties of hardware and software by predicate abstraction and model checking. ICCAD 2004: 437-438 - [c85]Sanjit A. Seshia, Randal E. Bryant:
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. LICS 2004: 100-109 - [c84]Randal E. Bryant:
System modeling and verification with UCLID. MEMOCODE 2004: 3-4 - [c83]Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur:
Revisiting Positive Equality. TACAS 2004: 1-15 - [c82]Shuvendu K. Lahiri, Randal E. Bryant:
Constructing Quantified Invariants via Predicate Abstraction. VMCAI 2004: 267-281 - 2003
- [c81]Rune Møller Jensen, Manuela M. Veloso, Randal E. Bryant:
Guided Symbolic Universal Planning. ICAPS 2003: 123-132 - [c80]Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook:
A Symbolic Approach to Predicate Abstraction. CAV 2003: 141-153 - [c79]Sanjit A. Seshia, Randal E. Bryant:
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. CAV 2003: 154-166 - [c78]Shuvendu K. Lahiri, Randal E. Bryant:
Deductive Verification of Advanced Out-of-Order Microprocessors. CAV 2003: 341-353 - [c77]Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia:
Convergence Testing in Term-Level Bounded Model Checking. CHARME 2003: 348-362 - [c76]Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant:
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. DAC 2003: 425-430 - [c75]Amit Goel, Gagan Hasteer, Randal E. Bryant:
Symbolic representation with ordered function templates. DAC 2003: 431-435 - [c74]Amit Goel, Randal E. Bryant:
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis. DATE 2003: 10816-10821 - [c73]Randal E. Bryant:
Reasoning about Infinite State Systems Using Boolean Methods. FSTTCS 2003: 399-407 - 2002
- [c72]Rune Møller Jensen, Randal E. Bryant, Manuela M. Veloso:
SetA*: An Efficient BDD-Based Heuristic Search Algorithm. AAAI/IAAI 2002: 668-673 - [c71]Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia:
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. CAV 2002: 78-92 - [c70]Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant:
Deciding Separation Formulas with SAT. CAV 2002: 209-222 - [c69]Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant:
Modeling and Verification of Out-of-Order Microprocessors in UCLID. FMCAD 2002: 142-159 - 2001
- [c68]Miroslav N. Velev, Randal E. Bryant:
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. CAV 2001: 235-240 - [c67]Miroslav N. Velev, Randal E. Bryant:
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. DAC 2001: 226-231 - [c66]Clayton B. McDonald, Randal E. Bryant:
Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis. DAC 2001: 283-288 - [c65]Clayton B. McDonald, Randal E. Bryant:
A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells. ICCAD 2001: 501-506 - [c64]Randal E. Bryant, David R. O'Hallaron:
Introducing computer systems from a programmer's perspective. SIGCSE 2001: 90-94 - 2000
- [c63]Randal E. Bryant, Miroslav N. Velev:
Boolean Satisfiability with Transitivity Constraints. CAV 2000: 85-98 - [c62]Miroslav N. Velev, Randal E. Bryant:
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. DAC 2000: 112-117 - [c61]Clayton B. McDonald, Randal E. Bryant:
Symbolic timing simulation using cluster scheduling. DAC 2000: 254-259 - [c60]Chris Wilson, David L. Dill, Randal E. Bryant:
Symbolic Simulation with Approximate Values. FMCAD 2000: 470-485 - [c59]Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel:
A Theory of Consistency for Modular Synchronous Systems. FMCAD 2000: 486-504 - 1999
- [c58]Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron:
Optimizing Symbolic Model Checking for Constraint-Rich Models. CAV 1999: 328-340 - [c57]Randal E. Bryant, Steven M. German, Miroslav N. Velev:
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. CAV 1999: 470-482 - [c56]Miroslav N. Velev, Randal E. Bryant:
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. CHARME 1999: 37-53 - [c55]Miroslav N. Velev, Randal E. Bryant:
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. DAC 1999: 397-401 - [c54]Clayton B. McDonald, Randal E. Bryant:
Symbolic functional and timing verification of transistor-level circuits. ICCAD 1999: 526-530 - [c53]Randal E. Bryant, Steven M. German, Miroslav N. Velev:
Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. TABLEAUX 1999: 1-13 - [c52]Vishnu A. Patankar, Alok Jain, Randal E. Bryant:
Formal Verification of an ARM Processor. VLSI Design 1999: 282-287 - 1998
- [c51]Miroslav N. Velev, Randal E. Bryant:
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. ACSD 1998: 200-212 - [c50]Bwolen Yang, Yirng-An Chen, Randal E. Bryant, David R. O'Hallaron:
Space- and Time-Efficient BDD Construction via Working Set Control. ASP-DAC 1998: 423-432 - [c49]Yirng-An Chen, Randal E. Bryant:
Verification of Floating-Point Adders. CAV 1998: 488-499 - [c48]Randal E. Bryant, Gerry Musgrave:
User Experience with High Level Formal Verification (Panel). DAC 1998: 327 - [c47]Miroslav N. Velev, Randal E. Bryant:
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. FMCAD 1998: 18-35 - [c46]Bwolen Yang, Randal E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, Fabio Somenzi:
A Performance Study of BDD-Based Model Checking. FMCAD 1998: 255-289 - [c45]Miroslav N. Velev, Randal E. Bryant:
Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. ICCD 1998: 400-406 - [c44]Randal E. Bryant:
Formal Verification of Pipelined Processors. TACAS 1998: 1-4 - [c43]Miroslav N. Velev, Randal E. Bryant:
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. TACAS 1998: 136-150 - 1997
- [c42]Randal E. Bryant, Miroslav N. Velev:
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. ASIAN 1997: 18-31 - [c41]Manish Pandey, Randal E. Bryant:
Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. CAV 1997: 244-255 - [c40]Miroslav N. Velev, Randal E. Bryant, Alok Jain:
Efficient Modeling of Memory Arrays in Symbolic Simulation. CAV 1997: 388-399 - [c39]Kyle L. Nelson, Alok Jain, Randal E. Bryant:
Formal Verification of a Superscalar Execution Unit. DAC 1997: 161-166 - [c38]Manish Pandey, Richard Raimi, Randal E. Bryant, Magdy S. Abadir:
Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation. DAC 1997: 167-172 - [c37]Yirng-An Chen, Randal E. Bryant:
PHDD: an efficient graph representation for floating point circuit verification. ICCAD 1997: 2-7 - 1996
- [c36]Manish Pandey, Richard Raimi, Derek L. Beatty, Randal E. Bryant:
Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation. DAC 1996: 649-654 - [c35]Randal E. Bryant:
Bit-Level Analysis of an SRT Divider Circuit. DAC 1996: 661-665 - [c34]Alok Jain, Kyle L. Nelson, Randal E. Bryant:
Verifying Nondeterministic Implementations of Deterministic Systems. FMCAD 1996: 109-125 - [c33]Yirng-An Chen, Randal E. Bryant:
ACV: an arithmetic circuit verifier. ICCAD 1996: 361-365 - 1995
- [c32]Randal E. Bryant:
Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract). CAV 1995: 1-3 - [c31]Randal E. Bryant, Yirng-An Chen:
Verification of Arithmetic Circuits with Binary Moment Diagrams. DAC 1995: 535-541 - [c30]Samir Jain, Randal E. Bryant, Alok Jain:
Automatic Clock Abstraction from Sequential Circuits. DAC 1995: 707-711 - [c29]Randal E. Bryant:
Binary decision diagrams and beyond: enabling technologies for formal verification. ICCAD 1995: 236-243 - [c28]Manish Pandey, Alok Jain, Randal E. Bryant, Derek L. Beatty, Gary York, Samir Jain:
Extraction of finite state machines from transistor netlists by symbolic simulation. ICCD 1995: 596-601 - 1994
- [c27]Derek L. Beatty, Randal E. Bryant:
Formally Verifying a Microprocessor Using a Simulation Methodology. DAC 1994: 596-602 - [c26]Carl-Johan H. Seger, Randal E. Bryant:
Digital Circuit Verification Using Partially-Ordered State Models. ISMVL 1994: 2-7 - 1993
- [c25]Alok Jain, Randal E. Bryant:
Inverter minimization in multi-level logic networks. ICCAD 1993: 462-465 - [c24]Randal E. Bryant:
Symbolic Analysis Methods for Masks, Circuits, and Systems. ICCD 1993: 6-8 - [c23]Thomas J. Sheffler, Randal E. Bryant:
An Analysis of Hashing on Parallel and Vector Computers. ICPP (3) 1993: 29-36 - [c22]Randal E. Bryant, J. D. Tygar, Lawrence P. Huang:
Geometric characterization of series-parallel variable resistor networks. ISCAS 1993: 2678-2681 - 1992
- [c21]Randal E. Bryant:
Formal Verification: A Slow, but Certain Evolution. IFIP Congress (1) 1992: 712 - 1991
- [c20]Alok Jain, Randal E. Bryant:
Mapping Switch-Level Simulation onto Gate-Level Hardware Accelerators. DAC 1991: 219-222 - [c19]Randal E. Bryant, Derek L. Beatty, Carl-Johan H. Seger:
Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation. DAC 1991: 397-402 - [c18]Randal E. Bryant:
Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis. ICCAD 1991: 350-353 - 1990
- [c17]Randal E. Bryant, Carl-Johan H. Seger:
Formal Verification of Digital Circuits Using Symbolic Ternary System Models. CAV 1990: 33-43 - [c16]Karl S. Brace, Richard L. Rudell, Randal E. Bryant:
Efficient Implementation of a BDD Package. DAC 1990: 40-45 - [c15]Randal E. Bryant:
Symbolic Simulation - Techniques and Applications. DAC 1990: 517-521 - [c14]Randal E. Bryant, Carl-Johan H. Seger:
Formal Verification of Digital Circuits Using Symbolic Ternary System Models. CAV (DIMACS/AMS volume) 1990: 121-146 - 1989
- [c13]Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar:
Massively Parallel Switch-Level Simulation: A Feasibility Study. DAC 1989: 91-97 - [c12]Kyeongsoon Cho, Randal E. Bryant:
Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation. DAC 1989: 418-423 - [c11]Randal E. Bryant:
Silicon Compilers: How Well Have They Done, and Where Are They Headed? IFIP Congress 1989: 379 - [c10]Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar:
Logic Simulation on Massively Parallel Architectures. ISCA 1989: 336-343 - [c9]Randal E. Bryant:
Verification of Synchronous Circuits by Symbolic Logic Simulation. Hardware Specification, Verification and Synthesis 1989: 14-24 - 1988
- [c8]Randal E. Bryant:
CAD Tool Needs for System Designers. DAC 1988: 476 - [c7]Derek L. Beatty, Randal E. Bryant:
Fast Incremental Circuit Analysis Using Extracted Hierarchy. DAC 1988: 495-500 - [c6]Randal E. Bryant:
Data parallel switch-level simulation. ICCAD 1988: 354-357 - 1987
- [c5]Randal E. Bryant, Derek L. Beatty, Karl S. Brace, Kyeongsoon Cho, Thomas J. Sheffler:
COSMOS: A Compiled Simulator for MOS Circuits. DAC 1987: 9-16 - 1985
- [c4]Randal E. Bryant:
Symbolic manipulation of Boolean functions using a graphical representation. DAC 1985: 688-694 - [c3]Randal E. Bryant, Michael Dd. Schuster:
Performance evaluation of FMOSSIM, a concurrent switch-level fault simulator. DAC 1985: 715-719 - 1981
- [c2]Randal E. Bryant:
MOSSIM: A switch-level simulator for MOS LSI. DAC 1981: 786-790 - 1980
- [c1]Randal E. Bryant, Jack B. Dennis:
Concurrent programming. Operating Systems Engineering 1980: 426-451
Parts in Books or Collections
- 2018
- [p1]Randal E. Bryant:
Binary Decision Diagrams. Handbook of Model Checking 2018: 191-217
Editorship
- 1998
- [e1]Basant R. Chawla, Randal E. Bryant, Jan M. Rabaey:
Proceedings of the 35th Conference on Design Automation, Moscone center, San Francico, California, USA, June 15-19, 1998. ACM Press 1998, ISBN 0-89791-964-5 [contents]
Informal and Other Publications
- 2023
- [i11]Mate Soos, Randal E. Bryant:
Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination. CoRR abs/2304.04292 (2023) - [i10]Randal E. Bryant:
Notes on "Bounds on BDD-Based Bucket Elimination". CoRR abs/2306.10337 (2023) - 2021
- [i9]Randal E. Bryant, Marijn J. H. Heule:
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. CoRR abs/2105.00885 (2021) - 2020
- [i8]Randal E. Bryant, Randy H. Katz, Chase Hensel, Erwin P. Gianchandani:
From Data to Knowledge to Action: Enabling the Smart Grid. CoRR abs/2008.00055 (2020) - 2017
- [i7]Gregory D. Hager, Randal E. Bryant, Eric Horvitz, Maja J. Mataric, Vasant G. Honavar:
Advances in Artificial Intelligence Require Progress Across all of Computer Science. CoRR abs/1707.04352 (2017) - [i6]Randal E. Bryant:
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. CoRR abs/1710.06500 (2017) - 2005
- [i5]Sanjit A. Seshia, Randal E. Bryant:
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. CoRR abs/cs/0508044 (2005) - 2004
- [i4]Shuvendu K. Lahiri, Randal E. Bryant:
Predicate Abstraction with Indexed Predicates. CoRR cs.LO/0407006 (2004) - 2002
- [i3]Randal E. Bryant, Christoph Meinel:
Ordered Binary Decision Diagrams in Electronic Design Automation. Universität Trier, Mathematik/Informatik, Forschungsbericht 02-20 (2002) - 2000
- [i2]Randal E. Bryant, Miroslav N. Velev:
Boolean Satisfiability with Transitivity Constraints. CoRR cs.LO/0008001 (2000) - 1999
- [i1]Randal E. Bryant, Steven M. German, Miroslav N. Velev:
Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic. CoRR cs.LO/9910014 (1999)
Coauthor Index
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-11 20:12 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
