Randal E. Bryant
According to our database^{1},
Randal E. Bryant
authored at least 132 papers
between 1980 and 2019.
Collaborative distances:
Collaborative distances:
Awards
ACM Fellow
ACM Fellow 2000, "Randal Bryant is best known for Ordered Binary Decision Diagrams, a canonical form for boolean functions. Although originally developed for applications in CAD, this data structure has found many applications in areas such as hardware and software verification, automated theorem proving, and AI planning.".
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at orcid.org

at id.loc.gov

at dnb.info

at isni.org

at dl.acm.org
On csauthors.net:
Bibliography
2019
Nonsilicon, Nonvon Neumann Computing  Part I [Scanning the Issue].
Proceedings of the IEEE, 2019
2018
Binary Decision Diagrams.
Proceedings of the Handbook of Model Checking., 2018
Chain Reduction for Binary and ZeroSuppressed Decision Diagrams.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018
Implementing Malloc: Students and Systems Programming.
Proceedings of the 49th ACM Technical Symposium on Computer Science Education, 2018
2017
Parallel discrete event simulation: The making of a field.
Proceedings of the 2017 Winter Simulation Conference, 2017
2016
EduPar 2016 Keynote.
Proceedings of the 2016 IEEE International Parallel and Distributed Processing Symposium Workshops, 2016
2013
Parrot: a practical runtime for deterministic, stable, and reliable threads.
Proceedings of the ACM SIGOPS 24th Symposium on Operating Systems Principles, 2013
2011
DataIntensive Scalable Computing for Scientific Applications.
Computing in Science and Engineering, 2011
Learning conditional abstractions.
Proceedings of the International Conference on Formal Methods in ComputerAided Design, 2011
2010
2009 CAV award announcement.
Formal Methods in System Design, 2010
ATLAS: Automatic Termlevel abstraction of RTL designs.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010
2009
An abstractionbased decision procedure for bitvector arithmetic.
STTT, 2009
The 2008 CAV Award citation.
Formal Methods in System Design, 2009
2008
Stateset branching: Leveraging BDDs for heuristic search.
Artif. Intell., 2008
A View from the Engine Room: Computational Support for Symbolic Model Checking.
Proceedings of the 25 Years of Model Checking  History, Achievements, Perspectives, 2008
2007
Predicate abstraction with indexed predicates.
ACM Trans. Comput. Log., 2007
On Solving Boolean Combinations of UTVPI Constraints.
JSAT, 2007
Deciding BitVector Arithmetic with Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007
2006
Formal Verification of Infinite State Systems Using Boolean Methods.
Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006
Formal Verification of Infinite State Systems Using Boolean Methods.
Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006
2005
TLSim and EVC: a termlevel symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories.
IJES, 2005
SemanticsAware Malware Detection.
Proceedings of the 2005 IEEE Symposium on Security and Privacy (S&P 2005), 2005
Automatic discovery of APIlevel exploits.
Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 2005
Decision Procedures Customized for Formal Verification.
Proceedings of the Automated Deduction, 2005
Modeling and Verifying Circuits Using Generalized Relative Timing.
Proceedings of the 11th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2005), 2005
2004
Constructing Quantified Invariants via Predicate Abstraction.
Proceedings of the Verification, 2004
Revisiting Positive Equality.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004
System modeling and verification with UCLID.
Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for CoDesign (MEMOCODE 2004), 2004
Deciding QuantifierFree Presburger Formulas Using Parameterized Solution Bounds.
Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004
Verifying properties of hardware and software by predicate abstraction and model checking.
Proceedings of the 2004 International Conference on ComputerAided Design, 2004
Indexed Predicate Discovery for Unbounded System Verification.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004
Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic NonDeterministic Planning.
Proceedings of the Fourteenth International Conference on Automated Planning and Scheduling (ICAPS 2004), 2004
2003
Reasoning about Infinite State Systems Using Boolean Methods.
Proceedings of the FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 2003
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis.
Proceedings of the 2003 Design, 2003
A hybrid SATbased decision procedure for separation logic with uninterpreted functions.
Proceedings of the 40th Design Automation Conference, 2003
Symbolic representation with ordered function templates.
Proceedings of the 40th Design Automation Conference, 2003
Convergence Testing in TermLevel Bounded Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 2003
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003
A Symbolic Approach to Predicate Abstraction.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003
Deductive Verification of Advanced OutofOrder Microprocessors.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003
Guided Symbolic Universal Planning.
Proceedings of the Thirteenth International Conference on Automated Planning and Scheduling (ICAPS 2003), 2003
Computer systems  a programmers perspective.
Pearson Education, ISBN: 9780131784567, 2003
2002
Ordered Binary Decision Diagrams in Electronic Design Automation
Universität Trier, Mathematik/Informatik, Forschungsbericht, 2002
Modeling and Verification of OutofOrder Microprocessors in UCLID.
Proceedings of the Formal Methods in ComputerAided Design, 4th International Conference, 2002
Deciding Separation Formulas with SAT.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002
SetA*: An Efficient BDDBased Heuristic Search Algorithm.
Proceedings of the Eighteenth National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence, July 28, 2002
2001
Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic.
ACM Trans. Comput. Log., 2001
CMOS circuit verification with symbolic switchlevel timingsimulation.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2001
An efficient graph representation for arithmetic circuitverification.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2001
Verification of arithmetic circuits using binary moment diagrams.
STTT, 2001
Introducing computer systems from a programmer's perspective.
Proceedings of the 32rd SIGCSE Technical Symposium on Computer Science Education, 2001
A Symbolic SimulationBased Methodology for Generating BlackBox Timing Models of Custom Macrocells.
Proceedings of the 2001 IEEE/ACM International Conference on ComputerAided Design, 2001
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors.
Proceedings of the 38th Design Automation Conference, 2001
Computing LogicStage Delays Using Circuit Simulation and Symbolic Elmore Analysis.
Proceedings of the 38th Design Automation Conference, 2001
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001
2000
Symbolic Simulation with Approximate Values.
Proceedings of the Formal Methods in ComputerAided Design, Third International Conference, 2000
A Theory of Consistency for Modular Synchronous Systems.
Proceedings of the Formal Methods in ComputerAided Design, Third International Conference, 2000
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction.
Proceedings of the 37th Conference on Design Automation, 2000
Symbolic timing simulation using cluster scheduling.
Proceedings of the 37th Conference on Design Automation, 2000
Boolean Satisfiability with Transitivity Constraints.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000
1999
Exploiting symmetry when verifying transistorlevel circuits by symbolic trajectory evaluation.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1999
Formal Verification of an ARM Processor.
Proceedings of the 12th International Conference on VLSI Design (VLSI Design 1999), 1999
Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1999
Symbolic functional and timing verification of transistorlevel circuits.
Proceedings of the 1999 IEEE/ACM International Conference on ComputerAided Design, 1999
Exploiting Positive Equality and Partial NonConsistency in the Formal Verification of Pipelined Microprocessors.
Proceedings of the 36th Conference on Design Automation, 1999
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic.
Proceedings of the Correct Hardware Design and Verification Methods, 1999
Optimizing Symbolic Model Checking for ConstraintRich Models.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999
1998
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998
Formal Verification of Pipelined Processors.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998
Incorporating timing constraints in the efficient memory model for symbolic ternary simulation.
Proceedings of the International Conference on Computer Design: VLSI in Computers and Processors, 1998
A Performance Study of BDDBased Model Checking.
Proceedings of the Formal Methods in ComputerAided Design, 1998
BitLevel Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking.
Proceedings of the Formal Methods in ComputerAided Design, 1998
User Experience with High Level Formal Verification (Panel).
Proceedings of the 35th Conference on Design Automation, 1998
Verification of FloatingPoint Adders.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998
Space and TimeEfficient BDD Construction via Working Set Control.
Proceedings of the ASPDAC '98, 1998
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation.
Proceedings of the 1st International Conference on Application of Concurrency to System Design (ACSD '98), 1998
1997
PHDD: an efficient graph representation for floating point circuit verification.
Proceedings of the 1997 IEEE/ACM International Conference on ComputerAided Design, 1997
Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation.
Proceedings of the 34st Conference on Design Automation, 1997
Formal Verification of a Superscalar Execution Unit.
Proceedings of the 34st Conference on Design Automation, 1997
Efficient Modeling of Memory Arrays in Symbolic Simulation.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997
Exploiting Symmetry When Verifying TransitorLevel Circuits by Symbolic Trajectory Evaluation.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation.
Proceedings of the Advances in Computing Science, 1997
1996
ACV: an arithmetic circuit verifier.
Proceedings of the 1996 IEEE/ACM International Conference on ComputerAided Design, 1996
Verifying Nondeterministic Implementations of Deterministic Systems.
Proceedings of the Formal Methods in ComputerAided Design, First International Conference, 1996
Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation.
Proceedings of the 33st Conference on Design Automation, 1996
BitLevel Analysis of an SRT Divider Circuit.
Proceedings of the 33st Conference on Design Automation, 1996
1995
Formal Verification by Symbolic Evaluation of PartiallyOrdered Trajectories.
Formal Methods in System Design, 1995
Extraction of finite state machines from transistor netlists by symbolic simulation.
Proceedings of the 1995 International Conference on Computer Design (ICCD '95), 1995
Binary decision diagrams and beyond: enabling technologies for formal verification.
Proceedings of the 1995 IEEE/ACM International Conference on ComputerAided Design, 1995
Automatic Clock Abstraction from Sequential Circuits.
Proceedings of the 32st Conference on Design Automation, 1995
Verification of Arithmetic Circuits with Binary Moment Diagrams.
Proceedings of the 32st Conference on Design Automation, 1995
Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract).
Proceedings of the Computer Aided Verification, 1995
1994
Digital Circuit Verification Using PartiallyOrdered State Models.
Proceedings of the 24th IEEE International Symposium on MultipleValued Logic, 1994
Formally Verifying a Microprocessor Using a Simulation Methodology.
Proceedings of the 31st Conference on Design Automation, 1994
1993
Intractability in linear switchlevel simulation.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1993
Geometric characterization of seriesparallel variable resistor networks.
Proceedings of the 1993 IEEE International Symposium on Circuits and Systems, 1993
An Analysis of Hashing on Parallel and Vector Computers.
Proceedings of the 1993 International Conference on Parallel Processing, 1993
Symbolic Analysis Methods for Masks, Circuits, and Systems.
Proceedings of the Proceedings 1993 International Conference on Computer Design: VLSI in Computers & Processors, 1993
Inverter minimization in multilevel logic networks.
Proceedings of the 1993 IEEE/ACM International Conference on ComputerAided Design, 1993
1992
Symbolic Boolean Manipulation with Ordered BinaryDecision Diagrams.
ACM Comput. Surv., 1992
Formal Verification: A Slow, but Certain Evolution.
Proceedings of the Algorithms, Software, Architecture, 1992
1991
Formal verification of memory circuits by switchlevel simulation.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1991
On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication.
IEEE Trans. Computers, 1991
A Methodology for Hardware Verification Based on Logic Simulation.
J. ACM, 1991
Extraction of Gate Level Models from Transistor Circuits by FourValued Symbolic Analysis.
Proceedings of the 1991 IEEE/ACM International Conference on ComputerAided Design, 1991
Mapping SwitchLevel Simulation onto GateLevel Hardware Accelerators.
Proceedings of the 28th Design Automation Conference, 1991
Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation.
Proceedings of the 28th Design Automation Conference, 1991
1990
Formal Verification of Digital Circuits Using Symbolic Ternary System Models.
Proceedings of the ComputerAided Verification, 1990
Symbolic Simulation  Techniques and Applications.
Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, 1990
Efficient Implementation of a BDD Package.
Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, 1990
Formal Verification of Digital Circuits Using Symbolic Ternary System Models.
Proceedings of the Computer Aided Verification, 2nd International Workshop, 1990
1989
Verification of Synchronous Circuits by Symbolic Logic Simulation.
Proceedings of the Hardware Specification, 1989
Logic Simulation on Massively Parallel Architectures.
Proceedings of the 16th Annual International Symposium on Computer Architecture. Jerusalem, 1989
Silicon Compilers: How Well Have They Done, and Where Are They Headed?
Proceedings of the Information Processing 89, Proceedings of the IFIP 11th World Computer Congress, San Francisco, USA, August 28, 1989
Massively Parallel SwitchLevel Simulation: A Feasibility Study.
Proceedings of the 26th ACM/IEEE Design Automation Conference, 1989
Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation.
Proceedings of the 26th ACM/IEEE Design Automation Conference, 1989
1988
Data parallel switchlevel simulation.
Proceedings of the 1988 IEEE International Conference on ComputerAided Design, 1988
CAD Tool Needs for System Designers.
Proceedings of the 25th ACM/IEEE Conference on Design Automation, 1988
Fast Incremental Circuit Analysis Using Extracted Hierarchy.
Proceedings of the 25th ACM/IEEE Conference on Design Automation, 1988
1987
Boolean Analysis of MOS Circuits.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1987
Algorithmic Aspects of Symbolic Switch Network Analysis.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1987
COSMOS: A Compiled Simulator for MOS Circuits.
Proceedings of the 24th ACM/IEEE Design Automation Conference. Miami Beach, FL, USA, June 28, 1987
1986
GraphBased Algorithms for Boolean Function Manipulation.
IEEE Trans. Computers, 1986
1985
A Hardware Architecture for SwitchLevel Simulation.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1985
Performance evaluation of FMOSSIM, a concurrent switchlevel fault simulator.
Proceedings of the 22nd ACM/IEEE conference on Design automation, 1985
Symbolic manipulation of Boolean functions using a graphical representation.
Proceedings of the 22nd ACM/IEEE conference on Design automation, 1985
1984
A SwitchLevel Model and Simulator for MOS Digital Systems.
IEEE Trans. Computers, 1984
1981
MOSSIM: A switchlevel simulator for MOS LSI.
Proceedings of the 18th Design Automation Conference, 1981
1980
Concurrent programming.
Proceedings of the Operating Systems Engineering: Proceedings of the 14th IBM Computer SCience Symposium, 1980