Randal E. Bryant
Orcid: 0000000150246613Affiliations:
 Carnegie Mellon University, Pittsburgh, USA
According to our database^{1},
Randal E. Bryant
authored at least 146 papers
between 1980 and 2023.
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.".
IEEE Fellow
IEEE Fellow 1990, "For contributions to switchlevel modeling of verylargescale integrated circuits.".
Timeline
Legend:
Book In proceedings Article PhD thesis Dataset OtherLinks
Online presence:

on orcid.org

on id.loc.gov

on dnb.info

on isni.org

on dl.acm.org
On csauthors.net:
Bibliography
2023
ACM Trans. Comput. Log., October, 2023
J. Autom. Reason., September, 2023
CoRR, 2023
CoRR, 2023
Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023
2022
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022
Proceedings of the 22nd Formal Methods in ComputerAided Design, 2022
2021
Proceedings of the Automated Deduction  CADE 28, 2021
2020
Proc. IEEE, 2020
J. Autom. Reason., 2020
CoRR, 2020
2019
Proc. IEEE, 2019
2018
Proceedings of the Handbook of Model Checking., 2018
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
Proceedings of the 2017 Winter Simulation Conference, 2017
2016
Proceedings of the 2016 IEEE International Parallel and Distributed Processing Symposium Workshops, 2016
2014
Interactions, 2014
2013
Proceedings of the ACM SIGOPS 24th Symposium on Operating Systems Principles, 2013
2011
Comput. Sci. Eng., 2011
Proceedings of the International Conference on Formal Methods in ComputerAided Design, 2011
2010
Formal Methods Syst. Des., 2010
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010
2009
Int. J. Softw. Tools Technol. Transf., 2009
Formal Methods Syst. Des., 2009
2008
Artif. Intell., 2008
Proceedings of the 25 Years of Model Checking  History, Achievements, Perspectives, 2008
2007
ACM Trans. Comput. Log., 2007
J. Satisf. Boolean Model. Comput., 2007
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007
2006
Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006
2005
Log. Methods Comput. Sci., 2005
TLSim and EVC: a termlevel symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories.
Int. J. Embed. Syst., 2005
Proceedings of the 2005 IEEE Symposium on Security and Privacy (S&P 2005), 2005
Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 2005
Proceedings of the Automated Deduction, 2005
Proceedings of the 11th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2005), 2005
2004
Proceedings of the Verification, 2004
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004
Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for CoDesign (MEMOCODE 2004), 2004
Verifying properties of hardware and software by predicate abstraction and model checking.
Proceedings of the 2004 International Conference on ComputerAided Design, 2004
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
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
J. Symb. Comput., 2003
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
Proceedings of the 40th Design Automation Conference, 2003
Proceedings of the Correct Hardware Design and Verification Methods, 2003
Proceedings of the Computer Aided Verification, 15th International Conference, 2003
Proceedings of the Computer Aided Verification, 15th International Conference, 2003
Proceedings of the Computer Aided Verification, 15th International Conference, 2003
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
ACM Trans. Comput. Log., 2002
Proceedings of the Formal Methods in ComputerAided Design, 4th International Conference, 2002
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
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
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001
Int. J. Softw. Tools Technol. Transf., 2001
Proc. IEEE, 2001
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
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
Proceedings of the Formal Methods in ComputerAided Design, Third International Conference, 2000
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
Proceedings of the 37th Conference on Design Automation, 2000
1999
Exploiting symmetry when verifying transistorlevel circuits by symbolic trajectory evaluation.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999
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
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
Proceedings of the Computer Aided Verification, 11th International Conference, 1999
Proceedings of the Computer Aided Verification, 11th International Conference, 1999
1998
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998
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
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
Proceedings of the 35th Conference on Design Automation, 1998
Proceedings of the Computer Aided Verification, 10th International Conference, 1998
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
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
Proceedings of the 34st Conference on Design Automation, 1997
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
Proceedings of the 1996 IEEE/ACM International Conference on ComputerAided Design, 1996
Proceedings of the Formal Methods in ComputerAided Design, First International Conference, 1996
Proceedings of the 33st Conference on Design Automation, 1996
Proceedings of the 33st Conference on Design Automation, 1996
1995
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 ComputerAided Design, 1995
Proceedings of the 32st Conference on Design Automation, 1995
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
Proceedings of the 24th IEEE International Symposium on MultipleValued Logic, 1994
Proceedings of the 31st Conference on Design Automation, 1994
1993
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1993
Geometric characterization of seriesparallel variable resistor networks.
Proceedings of the 1993 IEEE International Symposium on Circuits and Systems, 1993
Proceedings of the 1993 International Conference on Parallel Processing, 1993
Proceedings of the Proceedings 1993 International Conference on Computer Design: VLSI in Computers & Processors, 1993
Proceedings of the 1993 IEEE/ACM International Conference on ComputerAided Design, 1993
1992
ACM Comput. Surv., 1992
Formal Verification: A Slow, but Certain Evolution.
Proceedings of the Algorithms, Software, Architecture, 1992
1991
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1991
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
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
Proceedings of the 28th Design Automation Conference, 1991
Proceedings of the 28th Design Automation Conference, 1991
1990
Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, 1990
Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, 1990
Proceedings of the Computer Aided Verification, 2nd International Workshop, 1990
1989
Proceedings of the Hardware Specification, 1989
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
Proceedings of the 26th ACM/IEEE Design Automation Conference, 1989
1988
IEEE Des. Test, 1988
Proceedings of the 1988 IEEE International Conference on ComputerAided Design, 1988
Proceedings of the 25th ACM/IEEE Conference on Design Automation, 1988
Proceedings of the 25th ACM/IEEE Conference on Design Automation, 1988
1987
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1987
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1987
IEEE Des. Test, 1987
Proceedings of the 24th ACM/IEEE Design Automation Conference. Miami Beach, FL, USA, June 28, 1987
1986
IEEE Trans. Computers, 1986
1985
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1985
Proceedings of the 22nd ACM/IEEE conference on Design automation, 1985
Proceedings of the 22nd ACM/IEEE conference on Design automation, 1985
1984
IEEE Trans. Computers, 1984
1981
Proceedings of the 18th Design Automation Conference, 1981
1980
Proceedings of the Operating Systems Engineering: Proceedings of the 14th IBM Computer SCience Symposium, 1980