Search the dblp DataBase
Randal E. Bryant :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Randal E. Bryant Graph-Based Algorithms for Boolean Function Manipulation. [Citation Graph (4, 0)][DBLP ] IEEE Trans. Computers, 1986, v:35, n:8, pp:677-691 [Journal ] Randal E. Bryant Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. [Citation Graph (2, 0)][DBLP ] ACM Comput. Surv., 1992, v:24, n:3, pp:293-318 [Journal ] Rune M. Jensen , Randal E. Bryant , Manuela M. Veloso SetA*: An Efficient BDD-Based Heuristic Search Algorithm. [Citation Graph (0, 0)][DBLP ] AAAI/IAAI, 2002, pp:668-673 [Conf ] Miroslav N. Velev , Randal E. Bryant Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. [Citation Graph (0, 0)][DBLP ] ACSD, 1998, pp:200-212 [Conf ] Rune M. Jensen , Manuela M. Veloso , Randal E. Bryant Guided Symbolic Universal Planning. [Citation Graph (0, 0)][DBLP ] ICAPS, 2003, pp:123-132 [Conf ] Rune M. Jensen , Manuela M. Veloso , Randal E. Bryant Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic Non-Deterministic Planning. [Citation Graph (0, 0)][DBLP ] ICAPS, 2004, pp:335-344 [Conf ] Randal E. Bryant , Miroslav N. Velev Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. [Citation Graph (0, 0)][DBLP ] ASIAN, 1997, pp:18-31 [Conf ] Bwolen Yang , Yirng-An Chen , Randal E. Bryant , David R. O'Hallaron Space- and Time-Efficient BDD Construction via Working Set Control. [Citation Graph (0, 0)][DBLP ] ASP-DAC, 1998, pp:423-432 [Conf ] Sanjit A. Seshia , Randal E. Bryant , Kenneth S. Stevens Modeling and Verifying Circuits Using Generalized Relative Timing. [Citation Graph (0, 0)][DBLP ] ASYNC, 2005, pp:98-108 [Conf ] Randal E. Bryant , Sanjit A. Seshia Decision Procedures Customized for Formal Verification. [Citation Graph (0, 0)][DBLP ] CADE, 2005, pp:255-259 [Conf ] Randal E. Bryant Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract). [Citation Graph (0, 0)][DBLP ] CAV, 1995, pp:1-3 [Conf ] Randal E. Bryant , Steven M. German , Miroslav N. Velev Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. [Citation Graph (0, 0)][DBLP ] CAV, 1999, pp:470-482 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] CAV, 2002, pp:78-92 [Conf ] Randal E. Bryant , Carl-Johan H. Seger Formal Verification of Digital Circuits Using Symbolic Ternary System Models. [Citation Graph (0, 0)][DBLP ] CAV, 1990, pp:33-43 [Conf ] Randal E. Bryant , Miroslav N. Velev Boolean Satisfiability with Transitivity Constraints. [Citation Graph (0, 0)][DBLP ] CAV, 2000, pp:85-98 [Conf ] Yirng-An Chen , Randal E. Bryant Verification of Floating-Point Adders. [Citation Graph (0, 0)][DBLP ] CAV, 1998, pp:488-499 [Conf ] Amit Goel , Randal E. Bryant Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. [Citation Graph (0, 0)][DBLP ] CAV, 2004, pp:255-267 [Conf ] Shuvendu K. Lahiri , Randal E. Bryant Deductive Verification of Advanced Out-of-Order Microprocessors. [Citation Graph (0, 0)][DBLP ] CAV, 2003, pp:341-353 [Conf ] Shuvendu K. Lahiri , Randal E. Bryant Indexed Predicate Discovery for Unbounded System Verification. [Citation Graph (0, 0)][DBLP ] CAV, 2004, pp:135-147 [Conf ] Shuvendu K. Lahiri , Randal E. Bryant , Byron Cook A Symbolic Approach to Predicate Abstraction. [Citation Graph (0, 0)][DBLP ] CAV, 2003, pp:141-153 [Conf ] Manish Pandey , Randal E. Bryant Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. [Citation Graph (0, 0)][DBLP ] CAV, 1997, pp:244-255 [Conf ] Sanjit A. Seshia , Randal E. Bryant Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. [Citation Graph (0, 0)][DBLP ] CAV, 2003, pp:154-166 [Conf ] Ofer Strichman , Sanjit A. Seshia , Randal E. Bryant Deciding Separation Formulas with SAT. [Citation Graph (0, 0)][DBLP ] CAV, 2002, pp:209-222 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] CAV, 2001, pp:235-240 [Conf ] Miroslav N. Velev , Randal E. Bryant , Alok Jain Efficient Modeling of Memory Arrays in Symbolic Simulation. [Citation Graph (0, 0)][DBLP ] CAV, 1997, pp:388-399 [Conf ] Bwolen Yang , Reid G. Simmons , Randal E. Bryant , David R. O'Hallaron Optimizing Symbolic Model Checking for Constraint-Rich Models. [Citation Graph (0, 0)][DBLP ] CAV, 1999, pp:328-340 [Conf ] Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia Convergence Testing in Term-Level Bounded Model Checking. [Citation Graph (0, 0)][DBLP ] CHARME, 2003, pp:348-362 [Conf ] Miroslav N. Velev , Randal E. Bryant Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. [Citation Graph (0, 0)][DBLP ] CHARME, 1999, pp:37-53 [Conf ] Derek L. Beatty , Randal E. Bryant Fast Incremental Circuit Analysis Using Extracted Hierarchy. [Citation Graph (0, 0)][DBLP ] DAC, 1988, pp:495-500 [Conf ] Derek L. Beatty , Randal E. Bryant Formally Verifying a Microprocessor Using a Simulation Methodology. [Citation Graph (0, 0)][DBLP ] DAC, 1994, pp:596-602 [Conf ] Karl S. Brace , Richard L. Rudell , Randal E. Bryant Efficient Implementation of a BDD Package. [Citation Graph (0, 0)][DBLP ] DAC, 1990, pp:40-45 [Conf ] Randal E. Bryant CAD Tool Needs for System Designers. [Citation Graph (0, 0)][DBLP ] DAC, 1988, pp:476- [Conf ] Randal E. Bryant Symbolic Simulation - Techniques and Applications. [Citation Graph (0, 0)][DBLP ] DAC, 1990, pp:517-521 [Conf ] Randal E. Bryant Bit-Level Analysis of an SRT Divider Circuit. [Citation Graph (0, 0)][DBLP ] DAC, 1996, pp:661-665 [Conf ] Randal E. Bryant , Derek L. Beatty , Karl S. Brace , K. Cho , Thomas J. Sheffler COSMOS: A Compiled Simulator for MOS Circuits. [Citation Graph (0, 0)][DBLP ] DAC, 1987, pp:9-16 [Conf ] Randal E. Bryant , Derek L. Beatty , Carl-Johan H. Seger Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation. [Citation Graph (0, 0)][DBLP ] DAC, 1991, pp:397-402 [Conf ] Randal E. Bryant , Yirng-An Chen Verification of Arithmetic Circuits with Binary Moment Diagrams. [Citation Graph (0, 0)][DBLP ] DAC, 1995, pp:535-541 [Conf ] Randal E. Bryant , Gerry Musgrave User Experience with High Level Formal Verification (Panel). [Citation Graph (0, 0)][DBLP ] DAC, 1998, pp:327- [Conf ] K. Cho , Randal E. Bryant Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation. [Citation Graph (0, 0)][DBLP ] DAC, 1989, pp:418-423 [Conf ] Amit Goel , Gagan Hasteer , Randal E. Bryant Symbolic representation with ordered function templates. [Citation Graph (0, 0)][DBLP ] DAC, 2003, pp:431-435 [Conf ] Alok Jain , Randal E. Bryant Mapping Switch-Level Simulation onto Gate-Level Hardware Accelerators. [Citation Graph (0, 0)][DBLP ] DAC, 1991, pp:219-222 [Conf ] Samir Jain , Randal E. Bryant , Alok Jain Automatic Clock Abstraction from Sequential Circuits. [Citation Graph (0, 0)][DBLP ] DAC, 1995, pp:707-711 [Conf ] Saul A. Kravitz , Randal E. Bryant , Rob A. Rutenbar Massively Parallel Switch-Level Simulation: A Feasibility Study. [Citation Graph (0, 0)][DBLP ] DAC, 1989, pp:91-97 [Conf ] Clayton B. McDonald , Randal E. Bryant Symbolic timing simulation using cluster scheduling. [Citation Graph (0, 0)][DBLP ] DAC, 2000, pp:254-259 [Conf ] Clayton B. McDonald , Randal E. Bryant Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis. [Citation Graph (0, 0)][DBLP ] DAC, 2001, pp:283-288 [Conf ] Kyle L. Nelson , Alok Jain , Randal E. Bryant Formal Verification of a Superscalar Execution Unit. [Citation Graph (0, 0)][DBLP ] DAC, 1997, pp:161-166 [Conf ] Manish Pandey , Richard Raimi , Randal E. Bryant , Magdy S. Abadir Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation. [Citation Graph (0, 0)][DBLP ] DAC, 1997, pp:167-172 [Conf ] Manish Pandey , Richard Raimi , Derek L. Beatty , Randal E. Bryant Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation. [Citation Graph (0, 0)][DBLP ] DAC, 1996, pp:649-654 [Conf ] Sanjit A. Seshia , Shuvendu K. Lahiri , Randal E. Bryant A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. [Citation Graph (0, 0)][DBLP ] DAC, 2003, pp:425-430 [Conf ] Miroslav N. Velev , Randal E. Bryant Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. [Citation Graph (0, 0)][DBLP ] DAC, 2000, pp:112-117 [Conf ] Miroslav N. Velev , Randal E. Bryant Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. [Citation Graph (0, 0)][DBLP ] DAC, 2001, pp:226-231 [Conf ] Miroslav N. Velev , Randal E. Bryant Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. [Citation Graph (0, 0)][DBLP ] DAC, 1999, pp:397-401 [Conf ] Randal E. Bryant , Michael Dd. Schuster Performance evaluation of FMOSSIM, a concurrent switch-level fault simulator. [Citation Graph (0, 0)][DBLP ] DAC, 1985, pp:715-719 [Conf ] Randal E. Bryant Symbolic manipulation of Boolean functions using a graphical representation. [Citation Graph (0, 0)][DBLP ] DAC, 1985, pp:688-694 [Conf ] Amit Goel , Randal E. Bryant Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis. [Citation Graph (0, 0)][DBLP ] DATE, 2003, pp:10816-10821 [Conf ] Shuvendu K. Lahiri , Sanjit A. Seshia , Randal E. Bryant Modeling and Verification of Out-of-Order Microprocessors in UCLID. [Citation Graph (0, 0)][DBLP ] FMCAD, 2002, pp:142-159 [Conf ] Randal E. Bryant , Pankaj Chauhan , Edmund M. Clarke , Amit Goel A Theory of Consistency for Modular Synchronous Systems. [Citation Graph (0, 0)][DBLP ] FMCAD, 2000, pp:486-504 [Conf ] Alok Jain , Kyle L. Nelson , Randal E. Bryant Verifying Nondeterministic Implementations of Deterministic Systems. [Citation Graph (0, 0)][DBLP ] FMCAD, 1996, pp:109-125 [Conf ] Miroslav N. Velev , Randal E. Bryant Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. [Citation Graph (0, 0)][DBLP ] FMCAD, 1998, pp:18-35 [Conf ] Chris Wilson , David L. Dill , Randal E. Bryant Symbolic Simulation with Approximate Values. [Citation Graph (0, 0)][DBLP ] FMCAD, 2000, pp:470-485 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] FMCAD, 1998, pp:255-289 [Conf ] Randal E. Bryant Reasoning about Infinite State Systems Using Boolean Methods. [Citation Graph (0, 0)][DBLP ] FSTTCS, 2003, pp:399-407 [Conf ] Randal E. Bryant , Jack B. Dennis Concurrent programming. [Citation Graph (0, 0)][DBLP ] Operating Systems Engineering, 1980, pp:426-451 [Conf ] Randal E. Bryant Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis. [Citation Graph (0, 0)][DBLP ] ICCAD, 1991, pp:350-353 [Conf ] Randal E. Bryant Binary decision diagrams and beyond: enabling technologies for formal verification. [Citation Graph (0, 0)][DBLP ] ICCAD, 1995, pp:236-243 [Conf ] Randal E. Bryant , Sriram K. Rajamani Verifying properties of hardware and software by predicate abstraction and model checking. [Citation Graph (0, 0)][DBLP ] ICCAD, 2004, pp:437-438 [Conf ] Yirng-An Chen , Randal E. Bryant ACV: an arithmetic circuit verifier. [Citation Graph (0, 0)][DBLP ] ICCAD, 1996, pp:361-365 [Conf ] Yirng-An Chen , Randal E. Bryant PHDD: an efficient graph representation for floating point circuit verification. [Citation Graph (0, 0)][DBLP ] ICCAD, 1997, pp:2-7 [Conf ] Alok Jain , Randal E. Bryant Inverter minimization in multi-level logic networks. [Citation Graph (0, 0)][DBLP ] ICCAD, 1993, pp:462-465 [Conf ] Clayton B. McDonald , Randal E. Bryant A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells. [Citation Graph (0, 0)][DBLP ] ICCAD, 2001, pp:501-506 [Conf ] Clayton B. McDonald , Randal E. Bryant Symbolic functional and timing verification of transistor-level circuits. [Citation Graph (0, 0)][DBLP ] ICCAD, 1999, pp:526-530 [Conf ] Randal E. Bryant Symbolic Analysis Methods for Masks, Circuits, and Systems. [Citation Graph (0, 0)][DBLP ] ICCD, 1993, pp:6-8 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] ICCD, 1995, pp:596-601 [Conf ] Thomas J. Sheffler , Randal E. Bryant An Analysis of Hashing on Parallel and Vector Computers. [Citation Graph (0, 0)][DBLP ] ICPP, 1993, pp:29-36 [Conf ] Vinod Ganapathy , Sanjit A. Seshia , Somesh Jha , Thomas W. Reps , Randal E. Bryant Automatic discovery of API-level exploits. [Citation Graph (0, 0)][DBLP ] ICSE, 2005, pp:312-321 [Conf ] Randal E. Bryant Silicon Compilers: How Well Have They Done, and Where Are They Headed? [Citation Graph (0, 0)][DBLP ] IFIP Congress, 1989, pp:379- [Conf ] Randal E. Bryant Formal Verification: A Slow, but Certain Evolution. [Citation Graph (0, 0)][DBLP ] IFIP Congress (1), 1992, pp:712- [Conf ] Saul A. Kravitz , Randal E. Bryant , Rob A. Rutenbar Logic Simulation on Massively Parallel Architectures. [Citation Graph (0, 0)][DBLP ] ISCA, 1989, pp:336-343 [Conf ] Randal E. Bryant , J. D. Tygar , Lawrence P. Huang Geometric characterization of series-parallel variable resistor networks. [Citation Graph (0, 0)][DBLP ] ISCAS, 1993, pp:2678-2681 [Conf ] Carl-Johan H. Seger , Randal E. Bryant Digital Circuit Verification Using Partially-Ordered State Models. [Citation Graph (0, 0)][DBLP ] ISMVL, 1994, pp:2-7 [Conf ] Randal E. Bryant Formal Verification of Infinite State Systems Using Boolean Methods. [Citation Graph (0, 0)][DBLP ] LICS, 2006, pp:3-4 [Conf ] Sanjit A. Seshia , Randal E. Bryant Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. [Citation Graph (0, 0)][DBLP ] LICS, 2004, pp:100-109 [Conf ] Randal E. Bryant System modeling and verification with UCLID. [Citation Graph (0, 0)][DBLP ] MEMOCODE, 2004, pp:3-4 [Conf ] Randal E. Bryant Verification of Synchronous Circuits by Symbolic Logic Simulation. [Citation Graph (0, 0)][DBLP ] Hardware Specification, Verification and Synthesis, 1989, pp:14-24 [Conf ] Randal E. Bryant Formal Verification of Infinite State Systems Using Boolean Methods. [Citation Graph (0, 0)][DBLP ] RTA, 2006, pp:1-3 [Conf ] Randal E. Bryant , David R. O'Hallaron Introducing computer systems from a programmer's perspective. [Citation Graph (0, 0)][DBLP ] SIGCSE, 2001, pp:90-94 [Conf ] Mihai Christodorescu , Somesh Jha , Sanjit A. Seshia , Dawn Xiaodong Song , Randal E. Bryant Semantics-Aware Malware Detection. [Citation Graph (0, 0)][DBLP ] IEEE Symposium on Security and Privacy, 2005, pp:32-46 [Conf ] Randal E. Bryant , Steven M. German , Miroslav N. Velev Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. [Citation Graph (0, 0)][DBLP ] TABLEAUX, 1999, pp:1-13 [Conf ] Randal E. Bryant Formal Verification of Pipelined Processors. [Citation Graph (0, 0)][DBLP ] TACAS, 1998, pp:1-4 [Conf ] Shuvendu K. Lahiri , Randal E. Bryant , Amit Goel , Muralidhar Talupur Revisiting Positive Equality. [Citation Graph (0, 0)][DBLP ] TACAS, 2004, pp:1-15 [Conf ] Miroslav N. Velev , Randal E. Bryant Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. [Citation Graph (0, 0)][DBLP ] TACAS, 1998, pp:136-150 [Conf ] Vishnu A. Patankar , Alok Jain , Randal E. Bryant Formal Verification of an ARM Processor. [Citation Graph (0, 0)][DBLP ] VLSI Design, 1999, pp:282-287 [Conf ] Shuvendu K. Lahiri , Randal E. Bryant Constructing Quantified Invariants via Predicate Abstraction. [Citation Graph (0, 0)][DBLP ] VMCAI, 2004, pp:267-281 [Conf ] Randal E. Bryant , Miroslav N. Velev Boolean Satisfiability with Transitivity Constraints [Citation Graph (0, 0)][DBLP ] CoRR, 2000, v:0, n:, pp:- [Journal ] Shuvendu K. Lahiri , Randal E. Bryant Predicate Abstraction with Indexed Predicates [Citation Graph (0, 0)][DBLP ] CoRR, 2004, v:0, n:, pp:- [Journal ] Randal E. Bryant , Steven M. German , Miroslav N. Velev Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic [Citation Graph (0, 0)][DBLP ] CoRR, 1999, v:0, n:, pp:- [Journal ] Carl-Johan H. Seger , Randal E. Bryant Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 1995, v:6, n:2, pp:147-189 [Journal ] Randal E. Bryant A Methodology for Hardware Verification Based on Logic Simulation. [Citation Graph (0, 0)][DBLP ] J. ACM, 1991, v:38, n:2, pp:299-328 [Journal ] Miroslav N. Velev , Randal E. Bryant Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. [Citation Graph (0, 0)][DBLP ] J. Symb. Comput., 2003, v:35, n:2, pp:73-106 [Journal ] Sanjit A. Seshia , Randal E. Bryant Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. [Citation Graph (0, 0)][DBLP ] Logical Methods in Computer Science, 2005, v:1, n:2, pp:- [Journal ] Randal E. Bryant , Yirng-An Chen Verification of arithmetic circuits using binary moment diagrams. [Citation Graph (0, 0)][DBLP ] STTT, 2001, v:3, n:2, pp:137-155 [Journal ] Randal E. Bryant A Switch-Level Model and Simulator for MOS Digital Systems. [Citation Graph (0, 0)][DBLP ] IEEE Trans. Computers, 1984, v:33, n:2, pp:160-177 [Journal ] Randal E. Bryant On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication. [Citation Graph (0, 0)][DBLP ] IEEE Trans. Computers, 1991, v:40, n:2, pp:205-213 [Journal ] Randal E. Bryant Algorithmic Aspects of Symbolic Switch Network Analysis. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 1987, v:6, n:4, pp:618-633 [Journal ] Randal E. Bryant Boolean Analysis of MOS Circuits. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 1987, v:6, n:4, pp:634-649 [Journal ] Randal E. Bryant Formal verification of memory circuits by switch-level simulation. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 1991, v:10, n:1, pp:94-102 [Journal ] Yirng-An Chen , Randal E. Bryant An efficient graph representation for arithmetic circuitverification. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 2001, v:20, n:12, pp:1443-1454 [Journal ] William J. Dally , Randal E. Bryant A Hardware Architecture for Switch-Level Simulation. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 1985, v:4, n:3, pp:239-250 [Journal ] Lawrence P. Huang , Randal E. Bryant Intractability in linear switch-level simulation. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 1993, v:12, n:6, pp:829-836 [Journal ] Saul A. Kravitz , Randal E. Bryant , Rob A. Rutenbar Massively parallel switch-level simulation: a feasibility study. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 1991, v:10, n:7, pp:871-894 [Journal ] Clayton B. McDonald , Randal E. Bryant CMOS circuit verification with symbolic switch-level timingsimulation. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 2001, v:20, n:3, pp:458-474 [Journal ] Manish Pandey , Randal E. Bryant Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 1999, v:18, n:7, pp:918-935 [Journal ] Randal E. Bryant , Steven M. German , Miroslav N. Velev Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. [Citation Graph (0, 0)][DBLP ] ACM Trans. Comput. Log., 2001, v:2, n:1, pp:93-134 [Journal ] Randal E. Bryant , Miroslav N. Velev Boolean satisfiability with transitivity constraints. [Citation Graph (0, 0)][DBLP ] ACM Trans. Comput. Log., 2002, v:3, n:4, pp:604-627 [Journal ] Randal E. Bryant , Daniel Kroening , Joël Ouaknine , Sanjit A. Seshia , Ofer Strichman , Bryan A. Brady Deciding Bit-Vector Arithmetic with Abstraction. [Citation Graph (0, 0)][DBLP ] TACAS, 2007, pp:358-372 [Conf ] A View from the Engine Room: Computational Support for Symbolic Model Checking. [Citation Graph (, )][DBLP ] State-set branching: Leveraging BDDs for heuristic search. [Citation Graph (, )][DBLP ] Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds [Citation Graph (, )][DBLP ] Search in 0.019secs, Finished in 0.024secs