| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Randal E. Bryant |
Data-Intensive Scalable Computing for Scientific Applications.  |
Computing in Science and Engineering  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi |
2009 CAV award announcement. |
Formal Methods in System Design |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, John W. O'Leary |
ATLAS: Automatic Term-level abstraction of RTL designs. |
MEMOCODE |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2009 |
DBLP DOI BibTeX RDF |
Decision-procedures, Bit-vector |
| 1 | Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi |
The 2008 CAV Award citation. |
Formal Methods in System Design |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant |
State-set branching: Leveraging BDDs for heuristic search. |
Artif. Intell. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant |
A View from the Engine Room: Computational Support for Symbolic Model Checking. |
25 Years of Model Checking |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Sanjit A. Seshia, K. Subramani, Randal E. Bryant |
On Solving Boolean Combinations of UTVPI Constraints. |
JSAT |
2007 |
DBLP BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Randal E. Bryant |
Predicate abstraction with indexed predicates. |
ACM Trans. Comput. Log. |
2007 |
DBLP DOI BibTeX RDF |
infinite-state verification, invariant synthesis, Formal verification, abstract interpretation, cache-coherence protocols, predicate abstraction |
| 1 | Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady |
Deciding Bit-Vector Arithmetic with Abstraction. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant |
Formal Verification of Infinite State Systems Using Boolean Methods. |
RTA |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant |
Formal Verification of Infinite State Systems Using Boolean Methods. |
LICS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Sanjit A. Seshia, Randal E. Bryant |
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. |
Logical Methods in Computer Science |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Sanjit A. Seshia, Randal E. Bryant |
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds |
CoRR |
2005 |
DBLP BibTeX RDF |
|
| 1 | Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Xiaodong Song, Randal E. Bryant |
Semantics-Aware Malware Detection. |
IEEE Symposium on Security and Privacy |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Sanjit A. Seshia |
Decision Procedures Customized for Formal Verification. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Sanjit A. Seshia, Randal E. Bryant, Kenneth S. Stevens |
Modeling and Verifying Circuits Using Generalized Relative Timing. |
ASYNC |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant |
Automatic discovery of API-level exploits. |
ICSE |
2005 |
DBLP DOI BibTeX RDF |
API-level exploit, bounded model checking |
| 1 | Shuvendu K. Lahiri, Randal E. Bryant |
Predicate Abstraction with Indexed Predicates |
CoRR |
2004 |
DBLP BibTeX RDF |
|
| 1 | Randal E. Bryant |
System modeling and verification with UCLID. |
MEMOCODE |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur |
Revisiting Positive Equality. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant |
Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic Non-Deterministic Planning. |
ICAPS |
2004 |
DBLP BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Randal E. Bryant |
Indexed Predicate Discovery for Unbounded System Verification. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Amit Goel, Randal E. Bryant |
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Sanjit A. Seshia, Randal E. Bryant |
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. |
LICS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Randal E. Bryant |
Constructing Quantified Invariants via Predicate Abstraction. |
VMCAI |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Sriram K. Rajamani |
Verifying properties of hardware and software by predicate abstraction and model checking. |
ICCAD |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. |
J. Symb. Comput. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, David R. O'Hallaron |
Computer systems - a programmers perspective. |
|
2003 |
RDF |
|
| 1 | Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant |
Guided Symbolic Universal Planning. |
ICAPS |
2003 |
DBLP BibTeX RDF |
|
| 1 | Amit Goel, Gagan Hasteer, Randal E. Bryant |
Symbolic representation with ordered function templates. |
DAC |
2003 |
DBLP DOI BibTeX RDF |
function templates, logic design verification, boolean functions, binary decision diagrams, symbolic simulation |
| 1 | Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant |
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. |
DAC |
2003 |
DBLP DOI BibTeX RDF |
theorem proving, decision procedures, boolean satisfiability, design verification |
| 1 | Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia |
Convergence Testing in Term-Level Bounded Model Checking. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Amit Goel, Randal E. Bryant |
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis. |
DATE |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook |
A Symbolic Approach to Predicate Abstraction. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Sanjit A. Seshia, Randal E. Bryant |
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Randal E. Bryant |
Deductive Verification of Advanced Out-of-Order Microprocessors. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant |
Reasoning about Infinite State Systems Using Boolean Methods. |
FSTTCS |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Christoph Meinel |
Ordered Binary Decision Diagrams in Electronic Design Automation |
Universität Trier, Mathematik/Informatik, Forschungsbericht |
2002 |
RDF |
|
| 1 | Randal E. Bryant, Miroslav N. Velev |
Boolean satisfiability with transitivity constraints. |
ACM Trans. Comput. Log. |
2002 |
DBLP DOI BibTeX RDF |
formal verification, decision procedures, Boolean satisfiability |
| 1 | Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant |
Modeling and Verification of Out-of-Order Microprocessors in UCLID. |
FMCAD |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant |
Deciding Separation Formulas with SAT. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Rune M. Jensen, Randal E. Bryant, Manuela M. Veloso |
SetA*: An Efficient BDD-Based Heuristic Search Algorithm. |
AAAI/IAAI |
2002 |
DBLP BibTeX RDF |
|
| 1 | Clayton B. McDonald, Randal E. Bryant |
CMOS circuit verification with symbolic switch-level timingsimulation. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Yirng-An Chen, Randal E. Bryant |
An efficient graph representation for arithmetic circuitverification. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
2001 |
DBLP DOI BibTeX RDF |
processor verfication, decision procedures, uninterpreted functions |
| 1 | Randal E. Bryant, Yirng-An Chen |
Verification of arithmetic circuits using binary moment diagrams. |
STTT |
2001 |
DBLP DOI BibTeX RDF |
Formal verification, Computer arithmetic, Decision diagrams |
| 1 | Clayton B. McDonald, Randal E. Bryant |
Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis. |
DAC |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. |
DAC |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, David R. O'Hallaron |
Introducing computer systems from a programmer's perspective. |
SIGCSE |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Clayton B. McDonald, Randal E. Bryant |
A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells. |
ICCAD |
2001 |
DBLP BibTeX RDF |
|
| 1 | Randal E. Bryant, Miroslav N. Velev |
Boolean Satisfiability with Transitivity Constraints |
CoRR |
2000 |
DBLP BibTeX RDF |
|
| 1 | Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel |
A Theory of Consistency for Modular Synchronous Systems. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Chris Wilson, David L. Dill, Randal E. Bryant |
Symbolic Simulation with Approximate Values. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Clayton B. McDonald, Randal E. Bryant |
Symbolic timing simulation using cluster scheduling. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Miroslav N. Velev |
Boolean Satisfiability with Transitivity Constraints. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic |
CoRR |
1999 |
DBLP BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. |
DAC |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Vishnu A. Patankar, Alok Jain, Randal E. Bryant |
Formal Verification of an ARM Processor. |
VLSI Design |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron |
Optimizing Symbolic Model Checking for Constraint-Rich Models. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Clayton B. McDonald, Randal E. Bryant |
Symbolic functional and timing verification of transistor-level circuits. |
ICCAD |
1999 |
DBLP BibTeX RDF |
|
| 1 | Randal E. Bryant |
Formal Verification of Pipelined Processors. |
TACAS |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. |
TACAS |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. |
ACSD |
1998 |
DBLP DOI BibTeX RDF |
pipelined microprocessor verification, memory shadowing, Efficient Memory Model (EMM), circuit correspondence checking, symbolic simulation |
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant |
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. |
FMCAD |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Gerry Musgrave |
User Experience with High Level Formal Verification (Panel). |
DAC |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
DAC |
1998 |
DBLP BibTeX RDF |
|
| 1 | 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 |
DBLP BibTeX RDF |
|
| 1 | Yirng-An Chen, Randal E. Bryant |
Verification of Floating-Point Adders. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Miroslav N. Velev |
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. |
ASIAN |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Kyle L. Nelson, Alok Jain, Randal E. Bryant |
Formal Verification of a Superscalar Execution Unit. |
DAC |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Manish Pandey, Richard Raimi, Randal E. Bryant, Magdy S. Abadir |
Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation. |
DAC |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Miroslav N. Velev, Randal E. Bryant, Alok Jain |
Efficient Modeling of Memory Arrays in Symbolic Simulation. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Manish Pandey, Randal E. Bryant |
Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Yirng-An Chen, Randal E. Bryant |
PHDD: an efficient graph representation for floating point circuit verification. |
ICCAD |
1997 |
DBLP DOI BibTeX RDF |
KFDD, *BMD, HDD, K*BMD, Verification, Formal Verifications, BDD, Floating Point, FDD, BMD |
| 1 | Alok Jain, Kyle L. Nelson, Randal E. Bryant |
Verifying Nondeterministic Implementations of Deterministic Systems. |
FMCAD |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Manish Pandey, Richard Raimi, Derek L. Beatty, Randal E. Bryant |
Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation. |
DAC |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant |
Bit-Level Analysis of an SRT Divider Circuit. |
DAC |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Yirng-An Chen, Randal E. Bryant |
ACV: an arithmetic circuit verifier. |
ICCAD |
1996 |
DBLP DOI BibTeX RDF |
Binary Moment Diagram, Formal Verification, Arithmetic circuit, BMD, Hierarchical Verification |
| 1 | Carl-Johan H. Seger, Randal E. Bryant |
Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. |
Formal Methods in System Design |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Samir Jain, Randal E. Bryant, Alok Jain |
Automatic Clock Abstraction from Sequential Circuits. |
DAC |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Yirng-An Chen |
Verification of Arithmetic Circuits with Binary Moment Diagrams. |
DAC |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant |
Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract). |
CAV |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant |
Binary decision diagrams and beyond: enabling technologies for formal verification. |
ICCAD |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. (PDF / PS) |
ICCD |
1995 |
DBLP DOI BibTeX RDF |
finite state machine extraction, transistor netlists, clock level finite state machines, gate level representation, circuit clocking, output timing, simulation patterns, next state, output function, equivalent FSM, static storage structures, time multiplexed inputs, time multiplexed outputs, finite state machines, logic design, logic CAD, circuit analysis computing, FSMs, symbolic simulation, symbolic simulator, Ordered Binary Decision Diagrams |
| 1 | Derek L. Beatty, Randal E. Bryant |
Formally Verifying a Microprocessor Using a Simulation Methodology. |
DAC |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Carl-Johan H. Seger, Randal E. Bryant |
Digital Circuit Verification Using Partially-Ordered State Models. |
ISMVL |
1994 |
DBLP BibTeX RDF |
|
| 1 | Lawrence P. Huang, Randal E. Bryant |
Intractability in linear switch-level simulation. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas J. Sheffler, Randal E. Bryant |
An Analysis of Hashing on Parallel and Vector Computers. |
ICPP |
1993 |
DBLP BibTeX RDF |
|
| 1 | Randal E. Bryant, J. D. Tygar, Lawrence P. Huang |
Geometric characterization of series-parallel variable resistor networks. |
ISCAS |
1993 |
DBLP BibTeX RDF |
|
| 1 | Alok Jain, Randal E. Bryant |
Inverter minimization in multi-level logic networks. |
ICCAD |
1993 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")