Randal E. Bryant

Randal E. Bryant: Data-Intensive Scalable Computing for Scientific Applications. Computing in Science and Engineering 13(6): 25-33 (2011)

Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia: Learning conditional abstractions. FMCAD 2011: 116-124

Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi: 2009 CAV award announcement. Formal Methods in System Design 36(3): 195-197 (2010)

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

Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi: The 2008 CAV Award citation. Formal Methods in System Design 35(1): 4-5 (2009)

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. STTT 11(2): 95-104 (2009)

Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant: State-set branching: Leveraging BDDs for heuristic search. Artif. Intell. 172(2-3): 103-139 (2008)

Randal E. Bryant: A View from the Engine Room: Computational Support for Symbolic Model Checking. 25 Years of Model Checking 2008: 145-149

Sanjit A. Seshia, K. Subramani, Randal E. Bryant: On Solving Boolean Combinations of UTVPI Constraints. JSAT 3(1-2): 67-90 (2007)

Shuvendu K. Lahiri, Randal E. Bryant: Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. 9(1) (2007)

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

Randal E. Bryant: Formal Verification of Infinite State Systems Using Boolean Methods. LICS 2006: 3-4

Randal E. Bryant: Formal Verification of Infinite State Systems Using Boolean Methods. RTA 2006: 1-3

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. IJES 1(1/2): 134-149 (2005)

Sanjit A. Seshia, Randal E. Bryant: Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. Logical Methods in Computer Science 1(2) (2005)

Sanjit A. Seshia, Randal E. Bryant, Kenneth S. Stevens: Modeling and Verifying Circuits Using Generalized Relative Timing. ASYNC 2005: 98-108

Randal E. Bryant, Sanjit A. Seshia: Decision Procedures Customized for Formal Verification. CADE 2005: 255-259

Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant: Automatic discovery of API-level exploits. ICSE 2005: 312-321

Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Xiaodong Song, Randal E. Bryant: Semantics-Aware Malware Detection. IEEE Symposium on Security and Privacy 2005: 32-46

Sanjit A. Seshia, Randal E. Bryant: Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. CoRR abs/cs/0508044 (2005)

Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant: Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic Non-Deterministic Planning. ICAPS 2004: 335-344

Shuvendu K. Lahiri, Randal E. Bryant: Indexed Predicate Discovery for Unbounded System Verification. CAV 2004: 135-147

Amit Goel, Randal E. Bryant: Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. CAV 2004: 255-267

Randal E. Bryant, Sriram K. Rajamani: Verifying properties of hardware and software by predicate abstraction and model checking. ICCAD 2004: 437-438

Sanjit A. Seshia, Randal E. Bryant: Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. LICS 2004: 100-109

Randal E. Bryant: System modeling and verification with UCLID. MEMOCODE 2004: 3-4

Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur: Revisiting Positive Equality. TACAS 2004: 1-15

Shuvendu K. Lahiri, Randal E. Bryant: Constructing Quantified Invariants via Predicate Abstraction. VMCAI 2004: 267-281

Shuvendu K. Lahiri, Randal E. Bryant: Predicate Abstraction with Indexed Predicates. CoRR cs.LO/0407006 (2004)

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

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)

Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant: Guided Symbolic Universal Planning. ICAPS 2003: 123-132

Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook: A Symbolic Approach to Predicate Abstraction. CAV 2003: 141-153

Sanjit A. Seshia, Randal E. Bryant: Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. CAV 2003: 154-166

Shuvendu K. Lahiri, Randal E. Bryant: Deductive Verification of Advanced Out-of-Order Microprocessors. CAV 2003: 341-353

Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia: Convergence Testing in Term-Level Bounded Model Checking. CHARME 2003: 348-362

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

Amit Goel, Gagan Hasteer, Randal E. Bryant: Symbolic representation with ordered function templates. DAC 2003: 431-435

Amit Goel, Randal E. Bryant: Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis. DATE 2003: 10816-10821

Randal E. Bryant: Reasoning about Infinite State Systems Using Boolean Methods. FSTTCS 2003: 399-407

Randal E. Bryant, Miroslav N. Velev: Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3(4): 604-627 (2002)

Rune M. Jensen, Randal E. Bryant, Manuela M. Veloso: SetA*: An Efficient BDD-Based Heuristic Search Algorithm. AAAI/IAAI 2002: 668-673

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

Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant: Deciding Separation Formulas with SAT. CAV 2002: 209-222

Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant: Modeling and Verification of Out-of-Order Microprocessors in UCLID. FMCAD 2002: 142-159

Randal E. Bryant, Christoph Meinel: Ordered Binary Decision Diagrams in Electronic Design Automation. Universität Trier, Mathematik/Informatik, Forschungsbericht 02-20 (2002)

Randal E. Bryant, Yirng-An Chen: Verification of arithmetic circuits using binary moment diagrams. STTT 3(2): 137-155 (2001)

Clayton B. McDonald, Randal E. Bryant: CMOS circuit verification with symbolic switch-level timingsimulation. IEEE Trans. on CAD of Integrated Circuits and Systems 20(3): 458-474 (2001)

Yirng-An Chen, Randal E. Bryant: An efficient graph representation for arithmetic circuitverification. IEEE Trans. on CAD of Integrated Circuits and Systems 20(12): 1443-1454 (2001)

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)

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

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

Clayton B. McDonald, Randal E. Bryant: Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis. DAC 2001: 283-288

Clayton B. McDonald, Randal E. Bryant: A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells. ICCAD 2001: 501-506

Randal E. Bryant, David R. O'Hallaron: Introducing computer systems from a programmer's perspective. SIGCSE 2001: 90-94

Randal E. Bryant, Miroslav N. Velev: Boolean Satisfiability with Transitivity Constraints. CAV 2000: 85-98

Miroslav N. Velev, Randal E. Bryant: Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. DAC 2000: 112-117

Clayton B. McDonald, Randal E. Bryant: Symbolic timing simulation using cluster scheduling. DAC 2000: 254-259

Chris Wilson, David L. Dill, Randal E. Bryant: Symbolic Simulation with Approximate Values. FMCAD 2000: 470-485

Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel: A Theory of Consistency for Modular Synchronous Systems. FMCAD 2000: 486-504

Randal E. Bryant, Miroslav N. Velev: Boolean Satisfiability with Transitivity Constraints. CoRR cs.LO/0008001 (2000)

Manish Pandey, Randal E. Bryant: Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation. IEEE Trans. on CAD of Integrated Circuits and Systems 18(7): 918-935 (1999)

Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron: Optimizing Symbolic Model Checking for Constraint-Rich Models. CAV 1999: 328-340

Randal E. Bryant, Steven M. German, Miroslav N. Velev: Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. CAV 1999: 470-482

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

Miroslav N. Velev, Randal E. Bryant: Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. DAC 1999: 397-401

Clayton B. McDonald, Randal E. Bryant: Symbolic functional and timing verification of transistor-level circuits. ICCAD 1999: 526-530

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

Vishnu A. Patankar, Alok Jain, Randal E. Bryant: Formal Verification of an ARM Processor. VLSI Design 1999: 282-287

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)

Miroslav N. Velev, Randal E. Bryant: Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. ACSD 1998: 200-212

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

Yirng-An Chen, Randal E. Bryant: Verification of Floating-Point Adders. CAV 1998: 488-499

Randal E. Bryant, Gerry Musgrave: User Experience with High Level Formal Verification (Panel). DAC 1998: 327

Miroslav N. Velev, Randal E. Bryant: Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. FMCAD 1998: 18-35

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

Miroslav N. Velev, Randal E. Bryant: Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. ICCD 1998: 400-406

Randal E. Bryant: Formal Verification of Pipelined Processors. TACAS 1998: 1-4

Miroslav N. Velev, Randal E. Bryant: Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. TACAS 1998: 136-150

Basant R. Chawla, Randal E. Bryant, Jan M. Rabaey (Eds.): 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

Randal E. Bryant, Miroslav N. Velev: Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. ASIAN 1997: 18-31

Manish Pandey, Randal E. Bryant: Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. CAV 1997: 244-255

Miroslav N. Velev, Randal E. Bryant, Alok Jain: Efficient Modeling of Memory Arrays in Symbolic Simulation. CAV 1997: 388-399

Kyle L. Nelson, Alok Jain, Randal E. Bryant: Formal Verification of a Superscalar Execution Unit. DAC 1997: 161-166

Manish Pandey, Richard Raimi, Randal E. Bryant, Magdy S. Abadir: Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation. DAC 1997: 167-172

Yirng-An Chen, Randal E. Bryant: PHDD: an efficient graph representation for floating point circuit verification. ICCAD 1997: 2-7

Manish Pandey, Richard Raimi, Derek L. Beatty, Randal E. Bryant: Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation. DAC 1996: 649-654

Randal E. Bryant: Bit-Level Analysis of an SRT Divider Circuit. DAC 1996: 661-665

Alok Jain, Kyle L. Nelson, Randal E. Bryant: Verifying Nondeterministic Implementations of Deterministic Systems. FMCAD 1996: 109-125

Yirng-An Chen, Randal E. Bryant: ACV: an arithmetic circuit verifier. ICCAD 1996: 361-365

Carl-Johan H. Seger, Randal E. Bryant: Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Formal Methods in System Design 6(2): 147-189 (1995)

Randal E. Bryant: Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract). CAV 1995: 1-3

Randal E. Bryant, Yirng-An Chen: Verification of Arithmetic Circuits with Binary Moment Diagrams. DAC 1995: 535-541

Samir Jain, Randal E. Bryant, Alok Jain: Automatic Clock Abstraction from Sequential Circuits. DAC 1995: 707-711

Randal E. Bryant: Binary decision diagrams and beyond: enabling technologies for formal verification. ICCAD 1995: 236-243

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

Derek L. Beatty, Randal E. Bryant: Formally Verifying a Microprocessor Using a Simulation Methodology. DAC 1994: 596-602

Carl-Johan H. Seger, Randal E. Bryant: Digital Circuit Verification Using Partially-Ordered State Models. ISMVL 1994: 2-7

Lawrence P. Huang, Randal E. Bryant: Intractability in linear switch-level simulation. IEEE Trans. on CAD of Integrated Circuits and Systems 12(6): 829-836 (1993)

Alok Jain, Randal E. Bryant: Inverter minimization in multi-level logic networks. ICCAD 1993: 462-465

Randal E. Bryant: Symbolic Analysis Methods for Masks, Circuits, and Systems. ICCD 1993: 6-8

Thomas J. Sheffler, Randal E. Bryant: An Analysis of Hashing on Parallel and Vector Computers. ICPP 1993: 29-36

Randal E. Bryant, J. D. Tygar, Lawrence P. Huang: Geometric characterization of series-parallel variable resistor networks. ISCAS 1993: 2678-2681

Randal E. Bryant: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Comput. Surv. 24(3): 293-318 (1992)

Randal E. Bryant: Formal Verification: A Slow, but Certain Evolution. IFIP Congress (1) 1992: 712

Randal E. Bryant: A Methodology for Hardware Verification Based on Logic Simulation. J. ACM 38(2): 299-328 (1991)

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)

Randal E. Bryant: Formal verification of memory circuits by switch-level simulation. IEEE Trans. on CAD of Integrated Circuits and Systems 10(1): 94-102 (1991)

Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar: Massively parallel switch-level simulation: a feasibility study. IEEE Trans. on CAD of Integrated Circuits and Systems 10(7): 871-894 (1991)

Alok Jain, Randal E. Bryant: Mapping Switch-Level Simulation onto Gate-Level Hardware Accelerators. DAC 1991: 219-222

Randal E. Bryant, Derek L. Beatty, Carl-Johan H. Seger: Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation. DAC 1991: 397-402

Randal E. Bryant: Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis. ICCAD 1991: 350-353

Randal E. Bryant, Carl-Johan H. Seger: Formal Verification of Digital Circuits Using Symbolic Ternary System Models. CAV 1990: 33-43

Karl S. Brace, Richard L. Rudell, Randal E. Bryant: Efficient Implementation of a BDD Package. DAC 1990: 40-45

Randal E. Bryant: Symbolic Simulation - Techniques and Applications. DAC 1990: 517-521

Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar: Massively Parallel Switch-Level Simulation: A Feasibility Study. DAC 1989: 91-97

K. Cho, Randal E. Bryant: Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation. DAC 1989: 418-423

Randal E. Bryant: Silicon Compilers: How Well Have They Done, and Where Are They Headed? IFIP Congress 1989: 379

Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar: Logic Simulation on Massively Parallel Architectures. ISCA 1989: 336-343

Randal E. Bryant: Verification of Synchronous Circuits by Symbolic Logic Simulation. Hardware Specification, Verification and Synthesis 1989: 14-24

Randal E. Bryant: CAD Tool Needs for System Designers. DAC 1988: 476

Derek L. Beatty, Randal E. Bryant: Fast Incremental Circuit Analysis Using Extracted Hierarchy. DAC 1988: 495-500

Randal E. Bryant: Algorithmic Aspects of Symbolic Switch Network Analysis. IEEE Trans. on CAD of Integrated Circuits and Systems 6(4): 618-633 (1987)

Randal E. Bryant: Boolean Analysis of MOS Circuits. IEEE Trans. on CAD of Integrated Circuits and Systems 6(4): 634-649 (1987)

Randal E. Bryant, Derek L. Beatty, Karl S. Brace, K. Cho, Thomas J. Sheffler: COSMOS: A Compiled Simulator for MOS Circuits. DAC 1987: 9-16

Randal E. Bryant: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8): 677-691 (1986)

William J. Dally, Randal E. Bryant: A Hardware Architecture for Switch-Level Simulation. IEEE Trans. on CAD of Integrated Circuits and Systems 4(3): 239-250 (1985)

Randal E. Bryant: Symbolic manipulation of Boolean functions using a graphical representation. DAC 1985: 688-694

Randal E. Bryant, Michael Dd. Schuster: Performance evaluation of FMOSSIM, a concurrent switch-level fault simulator. DAC 1985: 715-719

Randal E. Bryant: A Switch-Level Model and Simulator for MOS Digital Systems. IEEE Trans. Computers 33(2): 160-177 (1984)

Randal E. Bryant: MOSSIM: A switch-level simulator for MOS LSI. DAC 1981: 786-790

Randal E. Bryant, Jack B. Dennis: Concurrent programming. Operating Systems Engineering 1980: 426-451