Randal E. Bryant

Orcid: 0000-0001-5024-6613

Affiliations:
  • Carnegie Mellon University, Pittsburgh, USA


According to our database1, Randal E. Bryant authored at least 147 papers between 1980 and 2024.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of three.

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.".

IEEE Fellow

IEEE Fellow 1990, "For contributions to switch-level modeling of very-large-scale integrated circuits.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
From Clauses to Klauses [inline-graphic not available: see fulltext].
Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023
Generating Extended Resolution Proofs with a BDD-Based SAT Solver.
ACM Trans. Comput. Log., October, 2023

Preprocessing of Propagation Redundant Clauses.
J. Autom. Reason., September, 2023

Notes on "Bounds on BDD-Based Bucket Elimination".
CoRR, 2023

Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination.
CoRR, 2023

Certified Knowledge Compilation with Application to Verified Model Counting.
Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

2022
Moving Definition Variables in Quantified Boolean Formulas.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Clausal Proofs for Pseudo-Boolean Reasoning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Tbuddy: A Proof-Generating BDD Package.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

2021
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver.
Proceedings of the Automated Deduction - CADE 28, 2021

2020
Nonsilicon, Non-von Neumann Computing - Part II.
Proc. IEEE, 2020

Chain Reduction for Binary and Zero-Suppressed Decision Diagrams.
J. Autom. Reason., 2020

From Data to Knowledge to Action: Enabling the Smart Grid.
CoRR, 2020

2019
Nonsilicon, Non-von Neumann Computing - Part I [Scanning the Issue].
Proc. IEEE, 2019

2018
Binary Decision Diagrams.
Proceedings of the Handbook of Model Checking., 2018

Implementing Malloc: Students and Systems Programming.
Proceedings of the 49th ACM Technical Symposium on Computer Science Education, 2018

2017
Advances in Artificial Intelligence Require Progress Across all of Computer Science.
CoRR, 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

2014
Antisocial computing: exploring design risks in social computing systems.
Interactions, 2014

2013
Parrot: a practical runtime for deterministic, stable, and reliable threads.
Proceedings of the ACM SIGOPS 24th Symposium on Operating Systems Principles, 2013

2011
Data-Intensive Scalable Computing for Scientific Applications.
Comput. Sci. Eng., 2011

Learning conditional abstractions.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

2010
2009 CAV award announcement.
Formal Methods Syst. Des., 2010

ATLAS: Automatic Term-level abstraction of RTL designs.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

2009
An abstraction-based decision procedure for bit-vector arithmetic.
Int. J. Softw. Tools Technol. Transf., 2009

The 2008 CAV Award citation.
Formal Methods Syst. Des., 2009

2008
State-set 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.
J. Satisf. Boolean Model. Comput., 2007

Deciding Bit-Vector 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 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

2005
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds.
Log. Methods Comput. Sci., 2005

TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories.
Int. J. Embed. Syst., 2005

Semantics-Aware Malware Detection.
Proceedings of the 2005 IEEE Symposium on Security and Privacy (S&P 2005), 2005

Automatic discovery of API-level 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 Co-Design (MEMOCODE 2004), 2004

Verifying properties of hardware and software by predicate abstraction and model checking.
Proceedings of the 2004 International Conference on Computer-Aided 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 Non-Deterministic Planning.
Proceedings of the Fourteenth International Conference on Automated Planning and Scheduling (ICAPS 2004), 2004

2003
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
J. Symb. Comput., 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 SAT-based 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 Term-Level 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 Out-of-Order 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: 978-0-13-178456-7, 2003

2002
Ordered Binary Decision Diagrams in Electronic Design Automation
Universität Trier, Mathematik/Informatik, Forschungsbericht, 2002

Boolean satisfiability with transitivity constraints.
ACM Trans. Comput. Log., 2002

Modeling and Verification of Out-of-Order Microprocessors in UCLID.
Proceedings of the Formal Methods in Computer-Aided 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 BDD-Based 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 switch-level timingsimulation.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001

An efficient graph representation for arithmetic circuitverification.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001

Verification of arithmetic circuits using binary moment diagrams.
Int. J. Softw. Tools Technol. Transf., 2001

Limitations and challenges of computer-aided design technology for CMOS VLSI.
Proc. IEEE, 2001

Introducing computer systems from a programmer's perspective.
Proceedings of the 32rd SIGCSE Technical Symposium on Computer Science Education, 2001

A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells.
Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, 2001

Computing Logic-Stage 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 Computer-Aided Design, Third International Conference, 2000

A Theory of Consistency for Modular Synchronous Systems.
Proceedings of the Formal Methods in Computer-Aided 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

1999
Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 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 transistor-level circuits.
Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Exploiting Positive Equality and Partial Non-Consistency 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 Constraint-Rich 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 BDD-Based Model Checking.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

User Experience with High Level Formal Verification (Panel).
Proceedings of the 35th Conference on Design Automation, 1998

Verification of Floating-Point Adders.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

Space- and Time-Efficient BDD Construction via Working Set Control.
Proceedings of the ASP-DAC '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 Computer-Aided 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 Transitor-Level 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 Computer-Aided Design, 1996

Verifying Nondeterministic Implementations of Deterministic Systems.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation.
Proceedings of the 33st Conference on Design Automation, 1996

Bit-Level Analysis of an SRT Divider Circuit.
Proceedings of the 33st Conference on Design Automation, 1996

1995
Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories.
Formal Methods Syst. Des., 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 Computer-Aided 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 Partially-Ordered State Models.
Proceedings of the 24th IEEE International Symposium on Multiple-Valued Logic, 1994

Formally Verifying a Microprocessor Using a Simulation Methodology.
Proceedings of the 31st Conference on Design Automation, 1994

1993
Intractability in linear switch-level simulation.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1993

Geometric characterization of series-parallel 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 multi-level logic networks.
Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993

1992
Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams.
ACM Comput. Surv., 1992

Formal Verification: A Slow, but Certain Evolution.
Proceedings of the Algorithms, Software, Architecture, 1992

1991
Massively parallel switch-level simulation: a feasibility study.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1991

Formal verification of memory circuits by switch-level simulation.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 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 Four-Valued Symbolic Analysis.
Proceedings of the 1991 IEEE/ACM International Conference on Computer-Aided Design, 1991

Mapping Switch-Level Simulation onto Gate-Level 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
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

Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation.
Proceedings of the 26th ACM/IEEE Design Automation Conference, 1989

1988
Incremental switch-level analysis.
IEEE Des. Test, 1988

Data parallel switch-level simulation.
Proceedings of the 1988 IEEE International Conference on Computer-Aided 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. Comput. Aided Des. Integr. Circuits Syst., 1987

Algorithmic Aspects of Symbolic Switch Network Analysis.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1987

A Survey of Switch-Level Algorithms.
IEEE Des. Test, 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
Graph-Based Algorithms for Boolean Function Manipulation.
IEEE Trans. Computers, 1986

1985
A Hardware Architecture for Switch-Level Simulation.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1985

Performance evaluation of FMOSSIM, a concurrent switch-level 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 Switch-Level Model and Simulator for MOS Digital Systems.
IEEE Trans. Computers, 1984

1981
MOSSIM: A switch-level 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


  Loading...