 | 2009 |
|---|
| 123 |       | 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) |
| 2008 |
|---|
| 122 | | Randal E. Bryant:
A View from the Engine Room: Computational Support for Symbolic Model Checking.
25 Years of Model Checking 2008: 145-149 |
| 121 | | 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) |
| 2007 |
|---|
| 120 | | 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 |
| 119 | | Shuvendu K. Lahiri,
Randal E. Bryant:
Predicate abstraction with indexed predicates.
ACM Trans. Comput. Log. 9(1): (2007) |
| 118 | | Sanjit A. Seshia,
K. Subramani,
Randal E. Bryant:
On Solving Boolean Combinations of UTVPI Constraints.
JSAT 3(1-2): 67-90 (2007) |
| 2006 |
|---|
| 117 | | Randal E. Bryant:
Formal Verification of Infinite State Systems Using Boolean Methods.
LICS 2006: 3-4 |
| 116 | | Randal E. Bryant:
Formal Verification of Infinite State Systems Using Boolean Methods.
RTA 2006: 1-3 |
| 2005 |
|---|
| 115 | | Sanjit A. Seshia,
Randal E. Bryant,
Kenneth S. Stevens:
Modeling and Verifying Circuits Using Generalized Relative Timing.
ASYNC 2005: 98-108 |
| 114 | | Randal E. Bryant,
Sanjit A. Seshia:
Decision Procedures Customized for Formal Verification.
CADE 2005: 255-259 |
| 113 | | Vinod Ganapathy,
Sanjit A. Seshia,
Somesh Jha,
Thomas W. Reps,
Randal E. Bryant:
Automatic discovery of API-level exploits.
ICSE 2005: 312-321 |
| 112 | | 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 |
| 111 | | Sanjit A. Seshia,
Randal E. Bryant:
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
CoRR abs/cs/0508044: (2005) |
| 110 | | 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) |
| 109 | | Sanjit A. Seshia,
Randal E. Bryant:
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds.
Logical Methods in Computer Science 1(2): (2005) |
| 2004 |
|---|
| 108 | | Shuvendu K. Lahiri,
Randal E. Bryant:
Indexed Predicate Discovery for Unbounded System Verification.
CAV 2004: 135-147 |
| 107 | | Amit Goel,
Randal E. Bryant:
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors.
CAV 2004: 255-267 |
| 106 |  | 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 |
| 105 | | Randal E. Bryant,
Sriram K. Rajamani:
Verifying properties of hardware and software by predicate abstraction and model checking.
ICCAD 2004: 437-438 |
| 104 | | Sanjit A. Seshia,
Randal E. Bryant:
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds.
LICS 2004: 100-109 |
| 103 | | Randal E. Bryant:
System modeling and verification with UCLID.
MEMOCODE 2004: 3-4 |
| 102 | | Shuvendu K. Lahiri,
Randal E. Bryant,
Amit Goel,
Muralidhar Talupur:
Revisiting Positive Equality.
TACAS 2004: 1-15 |
| 101 | | Shuvendu K. Lahiri,
Randal E. Bryant:
Constructing Quantified Invariants via Predicate Abstraction.
VMCAI 2004: 267-281 |
| 100 | | Shuvendu K. Lahiri,
Randal E. Bryant:
Predicate Abstraction with Indexed Predicates
CoRR cs.LO/0407006: (2004) |
| 2003 |
|---|
| 99 | | Shuvendu K. Lahiri,
Randal E. Bryant,
Byron Cook:
A Symbolic Approach to Predicate Abstraction.
CAV 2003: 141-153 |
| 98 | | Sanjit A. Seshia,
Randal E. Bryant:
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods.
CAV 2003: 154-166 |
| 97 | | Shuvendu K. Lahiri,
Randal E. Bryant:
Deductive Verification of Advanced Out-of-Order Microprocessors.
CAV 2003: 341-353 |
| 96 | | Randal E. Bryant,
Shuvendu K. Lahiri,
Sanjit A. Seshia:
Convergence Testing in Term-Level Bounded Model Checking.
CHARME 2003: 348-362 |
| 95 | | 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 |
| 94 | | Amit Goel,
Gagan Hasteer,
Randal E. Bryant:
Symbolic representation with ordered function templates.
DAC 2003: 431-435 |
| 93 | | Amit Goel,
Randal E. Bryant:
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis.
DATE 2003: 10816-10821 |
| 92 | | Randal E. Bryant:
Reasoning about Infinite State Systems Using Boolean Methods.
FSTTCS 2003: 399-407 |
| 91 | | Rune M. Jensen,
Manuela M. Veloso,
Randal E. Bryant:
Guided Symbolic Universal Planning.
ICAPS 2003: 123-132 |
| 90 | | 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 |
|---|
| 89 | | Rune M. Jensen,
Randal E. Bryant,
Manuela M. Veloso:
SetA*: An Efficient BDD-Based Heuristic Search Algorithm.
AAAI/IAAI 2002: 668-673 |
| 88 | | Ofer Strichman,
Sanjit A. Seshia,
Randal E. Bryant:
Deciding Separation Formulas with SAT.
CAV 2002: 209-222 |
| 87 | | 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 |
| 86 | | Shuvendu K. Lahiri,
Sanjit A. Seshia,
Randal E. Bryant:
Modeling and Verification of Out-of-Order Microprocessors in UCLID.
FMCAD 2002: 142-159 |
| 85 | | Randal E. Bryant,
Miroslav N. Velev:
Boolean satisfiability with transitivity constraints.
ACM Trans. Comput. Log. 3(4): 604-627 (2002) |
| 84 | | Randal E. Bryant,
Christoph Meinel:
Ordered Binary Decision Diagrams in Electronic Design Automation
Universität Trier, Mathematik/Informatik, Forschungsbericht 02-20: (2002) |
| 2001 |
|---|
| 83 | | 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 |
| 82 | | 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 |
| 81 | | Clayton B. McDonald,
Randal E. Bryant:
Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis.
DAC 2001: 283-288 |
| 80 | | Clayton B. McDonald,
Randal E. Bryant:
A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells.
ICCAD 2001: 501-506 |
| 79 | | Randal E. Bryant,
David R. O'Hallaron:
Introducing computer systems from a programmer's perspective.
SIGCSE 2001: 90-94 |
| 78 | | 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) |
| 77 | | 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) |
| 76 | | 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) |
| 75 | | Randal E. Bryant,
Yirng-An Chen:
Verification of arithmetic circuits using binary moment diagrams.
STTT 3(2): 137-155 (2001) |
| 2000 |
|---|
| 74 | | Randal E. Bryant,
Miroslav N. Velev:
Boolean Satisfiability with Transitivity Constraints.
CAV 2000: 85-98 |
| 73 | | Miroslav N. Velev,
Randal E. Bryant:
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction.
DAC 2000: 112-117 |
| 72 | | Clayton B. McDonald,
Randal E. Bryant:
Symbolic timing simulation using cluster scheduling.
DAC 2000: 254-259 |
| 71 | | Chris Wilson,
David L. Dill,
Randal E. Bryant:
Symbolic Simulation with Approximate Values.
FMCAD 2000: 470-485 |
| 70 | | Randal E. Bryant,
Pankaj Chauhan,
Edmund M. Clarke,
Amit Goel:
A Theory of Consistency for Modular Synchronous Systems.
FMCAD 2000: 486-504 |
| 69 | | Randal E. Bryant,
Miroslav N. Velev:
Boolean Satisfiability with Transitivity Constraints
CoRR cs.LO/0008001: (2000) |
| 1999 |
|---|
| 68 | | Bwolen Yang,
Reid G. Simmons,
Randal E. Bryant,
David R. O'Hallaron:
Optimizing Symbolic Model Checking for Constraint-Rich Models.
CAV 1999: 328-340 |
| 67 | | Randal E. Bryant,
Steven M. German,
Miroslav N. Velev:
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions.
CAV 1999: 470-482 |
| 66 | | 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 |
| 65 | | Miroslav N. Velev,
Randal E. Bryant:
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors.
DAC 1999: 397-401 |
| 64 | | Clayton B. McDonald,
Randal E. Bryant:
Symbolic functional and timing verification of transistor-level circuits.
ICCAD 1999: 526-530 |
| 63 | | 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 |
| 62 | | Vishnu A. Patankar,
Alok Jain,
Randal E. Bryant:
Formal Verification of an ARM Processor.
VLSI Design 1999: 282-287 |
| 61 | | 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) |
| 60 | | 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) |
| 1998 |
|---|
| 59 | | Miroslav N. Velev,
Randal E. Bryant:
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation.
ACSD 1998: 200-212 |
| 58 | | 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 |
| 57 | | Yirng-An Chen,
Randal E. Bryant:
Verification of Floating-Point Adders.
CAV 1998: 488-499 |
| 56 | | Randal E. Bryant,
Gerry Musgrave:
User Experience with High Level Formal Verification (Panel).
DAC 1998: 327 |
| 55 | | Miroslav N. Velev,
Randal E. Bryant:
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking.
FMCAD 1998: 18-35 |
| 54 | | 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 |
| 53 | | Randal E. Bryant:
Formal Verification of Pipelined Processors.
TACAS 1998: 1-4 |
| 52 | | Miroslav N. Velev,
Randal E. Bryant:
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation.
TACAS 1998: 136-150 |
| 1997 |
|---|
| 51 | | Randal E. Bryant,
Miroslav N. Velev:
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation.
ASIAN 1997: 18-31 |
| 50 | | Manish Pandey,
Randal E. Bryant:
Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation.
CAV 1997: 244-255 |
| 49 | | Miroslav N. Velev,
Randal E. Bryant,
Alok Jain:
Efficient Modeling of Memory Arrays in Symbolic Simulation.
CAV 1997: 388-399 |
| 48 | | Kyle L. Nelson,
Alok Jain,
Randal E. Bryant:
Formal Verification of a Superscalar Execution Unit.
DAC 1997: 161-166 |
| 47 | | Manish Pandey,
Richard Raimi,
Randal E. Bryant,
Magdy S. Abadir:
Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation.
DAC 1997: 167-172 |
| 46 | | Yirng-An Chen,
Randal E. Bryant:
PHDD: an efficient graph representation for floating point circuit verification.
ICCAD 1997: 2-7 |
| 1996 |
|---|
| 45 | | Manish Pandey,
Richard Raimi,
Derek L. Beatty,
Randal E. Bryant:
Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation.
DAC 1996: 649-654 |
| 44 | | Randal E. Bryant:
Bit-Level Analysis of an SRT Divider Circuit.
DAC 1996: 661-665 |
| 43 | | Alok Jain,
Kyle L. Nelson,
Randal E. Bryant:
Verifying Nondeterministic Implementations of Deterministic Systems.
FMCAD 1996: 109-125 |
| 42 | | Yirng-An Chen,
Randal E. Bryant:
ACV: an arithmetic circuit verifier.
ICCAD 1996: 361-365 |
| 1995 |
|---|
| 41 | | Randal E. Bryant:
Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract).
CAV 1995: 1-3 |
| 40 | | Randal E. Bryant,
Yirng-An Chen:
Verification of Arithmetic Circuits with Binary Moment Diagrams.
DAC 1995: 535-541 |
| 39 | | Samir Jain,
Randal E. Bryant,
Alok Jain:
Automatic Clock Abstraction from Sequential Circuits.
DAC 1995: 707-711 |
| 38 | | Randal E. Bryant:
Binary decision diagrams and beyond: enabling technologies for formal verification.
ICCAD 1995: 236-243 |
| 37 | | 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 |
| 36 | | 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) |
| 1994 |
|---|
| 35 | | Derek L. Beatty,
Randal E. Bryant:
Formally Verifying a Microprocessor Using a Simulation Methodology.
DAC 1994: 596-602 |
| 34 | | Carl-Johan H. Seger,
Randal E. Bryant:
Digital Circuit Verification Using Partially-Ordered State Models.
ISMVL 1994: 2-7 |
| 1993 |
|---|
| 33 | | Alok Jain,
Randal E. Bryant:
Inverter minimization in multi-level logic networks.
ICCAD 1993: 462-465 |
| 32 | | Randal E. Bryant:
Symbolic Analysis Methods for Masks, Circuits, and Systems.
ICCD 1993: 6-8 |
| 31 | | Thomas J. Sheffler,
Randal E. Bryant:
An Analysis of Hashing on Parallel and Vector Computers.
ICPP 1993: 29-36 |
| 30 | | Randal E. Bryant,
J. D. Tygar,
Lawrence P. Huang:
Geometric characterization of series-parallel variable resistor networks.
ISCAS 1993: 2678-2681 |
| 29 | | 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) |
| 1992 |
|---|
| 28 | | Randal E. Bryant:
Formal Verification: A Slow, but Certain Evolution.
IFIP Congress (1) 1992: 712 |
| 27 | | Randal E. Bryant:
Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams.
ACM Comput. Surv. 24(3): 293-318 (1992) |
| 1991 |
|---|
| 26 | | Alok Jain,
Randal E. Bryant:
Mapping Switch-Level Simulation onto Gate-Level Hardware Accelerators.
DAC 1991: 219-222 |
| 25 | | Randal E. Bryant,
Derek L. Beatty,
Carl-Johan H. Seger:
Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation.
DAC 1991: 397-402 |
| 24 | | Randal E. Bryant:
Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis.
ICCAD 1991: 350-353 |
| 23 | | 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) |
| 22 | | 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) |
| 21 | | 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) |
| 20 | | Randal E. Bryant:
A Methodology for Hardware Verification Based on Logic Simulation.
J. ACM 38(2): 299-328 (1991) |
| 1990 |
|---|
| 19 | | Randal E. Bryant,
Carl-Johan H. Seger:
Formal Verification of Digital Circuits Using Symbolic Ternary System Models.
CAV 1990: 33-43 |
| 18 | | Karl S. Brace,
Richard L. Rudell,
Randal E. Bryant:
Efficient Implementation of a BDD Package.
DAC 1990: 40-45 |
| 17 | | Randal E. Bryant:
Symbolic Simulation - Techniques and Applications.
DAC 1990: 517-521 |
| 1989 |
|---|
| 16 | | K. Cho,
Randal E. Bryant:
Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation.
DAC 1989: 418-423 |
| 15 | | Saul A. Kravitz,
Randal E. Bryant,
Rob A. Rutenbar:
Massively Parallel Switch-Level Simulation: A Feasibility Study.
DAC 1989: 91-97 |
| 14 | | Randal E. Bryant:
Verification of Synchronous Circuits by Symbolic Logic Simulation.
Hardware Specification, Verification and Synthesis 1989: 14-24 |
| 13 | | Randal E. Bryant:
Silicon Compilers: How Well Have They Done, and Where Are They Headed?
IFIP Congress 1989: 379 |
| 12 | | Saul A. Kravitz,
Randal E. Bryant,
Rob A. Rutenbar:
Logic Simulation on Massively Parallel Architectures.
ISCA 1989: 336-343 |
| 1988 |
|---|
| 11 | | Randal E. Bryant:
CAD Tool Needs for System Designers.
DAC 1988: 476 |
| 10 | | Derek L. Beatty,
Randal E. Bryant:
Fast Incremental Circuit Analysis Using Extracted Hierarchy.
DAC 1988: 495-500 |
| 1987 |
|---|
| 9 | | 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 |
| 8 | | Randal E. Bryant:
Algorithmic Aspects of Symbolic Switch Network Analysis.
IEEE Trans. on CAD of Integrated Circuits and Systems 6(4): 618-633 (1987) |
| 7 | | Randal E. Bryant:
Boolean Analysis of MOS Circuits.
IEEE Trans. on CAD of Integrated Circuits and Systems 6(4): 634-649 (1987) |
| 1986 |
|---|
| 6 | | Randal E. Bryant:
Graph-Based Algorithms for Boolean Function Manipulation.
IEEE Trans. Computers 35(8): 677-691 (1986) |
| 1985 |
|---|
| 5 | | Randal E. Bryant:
Symbolic manipulation of Boolean functions using a graphical representation.
DAC 1985: 688-694 |
| 4 | | Randal E. Bryant,
Michael Dd. Schuster:
Performance evaluation of FMOSSIM, a concurrent switch-level fault simulator.
DAC 1985: 715-719 |
| 3 | | 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) |
| 1984 |
|---|
| 2 | | Randal E. Bryant:
A Switch-Level Model and Simulator for MOS Digital Systems.
IEEE Trans. Computers 33(2): 160-177 (1984) |
| 1980 |
|---|
| 1 | | Randal E. Bryant,
Jack B. Dennis:
Concurrent programming.
Operating Systems Engineering 1980: 426-451 |
