Randal E. Bryant

ORCID

Publication Activity (10 Years)

Years Active: 1980-2024
Publications (10 Years): 23

Top Venues

Publications

Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
From Clauses to Klauses [inline-graphic not available: see fulltext]. CAV (1) (2024)
Mate Soos, Randal E. Bryant
Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination. CoRR (2023)
Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
Certified Knowledge Compilation with Application to Verified Model Counting. SAT (2023)
Randal E. Bryant
Notes on "Bounds on BDD-Based Bucket Elimination". CoRR (2023)
Randal E. Bryant, Marijn J. H. Heule
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. ACM Trans. Comput. Log. 24 (4) (2023)
Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
Preprocessing of Propagation Redundant Clauses. J. Autom. Reason. 67 (3) (2023)
Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
Preprocessing of Propagation Redundant Clauses. IJCAR (2022)
Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
Moving Definition Variables in Quantified Boolean Formulas. TACAS (1) (2022)
Randal E. Bryant
Tbuddy: A Proof-Generating BDD Package. FMCAD (2022)
Randal E. Bryant, Armin Biere, Marijn J. H. Heule
Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) (2022)
Randal E. Bryant, Marijn J. H. Heule
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. CoRR (2021)
Randal E. Bryant, Marijn J. H. Heule
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. CADE (2021)
Randal E. Bryant, Marijn J. H. Heule
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. TACAS (1) (2021)
Sankar Basu, Randal E. Bryant, Giovanni De Micheli, Thomas N. Theis, Lloyd Whitman
Nonsilicon, Non-von Neumann Computing - Part II. Proc. IEEE 108 (8) (2020)
Randal E. Bryant, Randy H. Katz, Chase Hensel, Erwin P. Gianchandani
From Data to Knowledge to Action: Enabling the Smart Grid. CoRR (2020)
Randal E. Bryant
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. J. Autom. Reason. 64 (7) (2020)
Sankar Basu, Randal E. Bryant, Giovanni De Micheli, Thomas N. Theis, Lloyd Whitman
Nonsilicon, Non-von Neumann Computing - Part I [Scanning the Issue]. Proc. IEEE 107 (1) (2019)
Brian P. Railing, Randal E. Bryant
Implementing Malloc: Students and Systems Programming. SIGCSE (2018)
Randal E. Bryant
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. TACAS (1) (2018)
Randal E. Bryant
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. CoRR (2017)
Richard M. Fujimoto, Rajive L. Bagrodia, Randal E. Bryant, K. Mani Chandy, David R. Jefferson, Jayadev Misra, David M. Nicol, Brian W. Unger
Parallel discrete event simulation: The making of a field. WSC (2017)
Gregory D. Hager, Randal E. Bryant, Eric Horvitz, Maja J. Mataric, Vasant G. Honavar
Advances in Artificial Intelligence Require Progress Across all of Computer Science. CoRR (2017)
Randal E. Bryant
EduPar 2016 Keynote. IPDPS Workshops (2016)
David W. McDonald, David H. Ackley, Randal E. Bryant, Melissa Gedney, Haym Hirsh, Lea Shanley
Antisocial computing: exploring design risks in social computing systems. Interactions 21 (6) (2014)
Heming Cui, Jirí Simsa, Yi-Hong Lin, Hao Li, Ben Blum, Xinan Xu, Junfeng Yang, Garth A. Gibson, Randal E. Bryant
Parrot: a practical runtime for deterministic, stable, and reliable threads. SOSP (2013)
Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia
Learning conditional abstractions. FMCAD (2011)
Randal E. Bryant
Data-Intensive Scalable Computing for Scientific Applications. Comput. Sci. Eng. 13 (6) (2011)
Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi
2009 CAV award announcement. Formal Methods Syst. Des. 36 (3) (2010)
Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, John W. O'Leary
ATLAS: Automatic Term-level abstraction of RTL designs. MEMOCODE (2010)
Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi
The 2008 CAV Award citation. Formal Methods Syst. Des. 35 (1) (2009)
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. Int. J. Softw. Tools Technol. Transf. 11 (2) (2009)
Randal E. Bryant
A View from the Engine Room: Computational Support for Symbolic Model Checking. 25 Years of Model Checking (2008)
Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant
State-set branching: Leveraging BDDs for heuristic search. Artif. Intell. 172 (2-3) (2008)
Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
Deciding Bit-Vector Arithmetic with Abstraction. TACAS (2007)
Sanjit A. Seshia, K. Subramani, Randal E. Bryant
On Solving Boolean Combinations of UTVPI Constraints. J. Satisf. Boolean Model. Comput. 3 (1-2) (2007)
Shuvendu K. Lahiri, Randal E. Bryant
Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. 9 (1) (2007)
Randal E. Bryant
Formal Verification of Infinite State Systems Using Boolean Methods. RTA (2006)
Randal E. Bryant
Formal Verification of Infinite State Systems Using Boolean Methods. LICS (2006)
Sanjit A. Seshia, Randal E. Bryant, Kenneth S. Stevens
Modeling and Verifying Circuits Using Generalized Relative Timing. ASYNC (2005)
Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant
Automatic discovery of API-level exploits. ICSE (2005)
Randal E. Bryant, Sanjit A. Seshia
Decision Procedures Customized for Formal Verification. CADE (2005)
Sanjit A. Seshia, Randal E. Bryant
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. Log. Methods Comput. Sci. 1 (2) (2005)
Sanjit A. Seshia, Randal E. Bryant
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds CoRR (2005)
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. Int. J. Embed. Syst. 1 (1/2) (2005)
Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Xiaodong Song, Randal E. Bryant
Semantics-Aware Malware Detection. IEEE Symposium on Security and Privacy (2005)
Shuvendu K. Lahiri, Randal E. Bryant
Indexed Predicate Discovery for Unbounded System Verification. CAV (2004)
Shuvendu K. Lahiri, Randal E. Bryant
Predicate Abstraction with Indexed Predicates CoRR (2004)
Randal E. Bryant
System modeling and verification with UCLID. MEMOCODE (2004)
Sanjit A. Seshia, Randal E. Bryant
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. LICS (2004)
Randal E. Bryant, Sriram K. Rajamani
Verifying properties of hardware and software by predicate abstraction and model checking. ICCAD (2004)
Amit Goel, Randal E. Bryant
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. CAV (2004)
Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur
Revisiting Positive Equality. TACAS (2004)
Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant
Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic Non-Deterministic Planning. ICAPS (2004)
Shuvendu K. Lahiri, Randal E. Bryant
Constructing Quantified Invariants via Predicate Abstraction. VMCAI (2004)
Shuvendu K. Lahiri, Randal E. Bryant
Deductive Verification of Advanced Out-of-Order Microprocessors. CAV (2003)
Randal E. Bryant
Reasoning about Infinite State Systems Using Boolean Methods. FSTTCS (2003)
Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. DAC (2003)
Amit Goel, Gagan Hasteer, Randal E. Bryant
Symbolic representation with ordered function templates. DAC (2003)
Amit Goel, Randal E. Bryant
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis. DATE (2003)
Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant
Guided Symbolic Universal Planning. ICAPS (2003)
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
Convergence Testing in Term-Level Bounded Model Checking. CHARME (2003)
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) (2003)
Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook
A Symbolic Approach to Predicate Abstraction. CAV (2003)
Sanjit A. Seshia, Randal E. Bryant
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. CAV (2003)
Randal E. Bryant, Miroslav N. Velev
Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3 (4) (2002)
Rune M. Jensen, Randal E. Bryant, Manuela M. Veloso
SetA*: An Efficient BDD-Based Heuristic Search Algorithm. AAAI/IAAI (2002)
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)
Randal E. Bryant, Christoph Meinel
Ordered Binary Decision Diagrams in Electronic Design Automation Universität Trier, Mathematik/Informatik, Forschungsbericht (2002)
Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant
Modeling and Verification of Out-of-Order Microprocessors in UCLID. FMCAD (2002)
Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant
Deciding Separation Formulas with SAT. CAV (2002)
Clayton B. McDonald, Randal E. Bryant
A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells. ICCAD (2001)
Clayton B. McDonald, Randal E. Bryant
CMOS circuit verification with symbolic switch-level timingsimulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20 (3) (2001)
Clayton B. McDonald, Randal E. Bryant
Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis. DAC (2001)
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)
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) (2001)
Randal E. Bryant, David R. O'Hallaron
Introducing computer systems from a programmer's perspective. SIGCSE (2001)
Randal E. Bryant, Kwang-Ting Cheng, Andrew B. Kahng, Kurt Keutzer, Wojciech Maly, A. Richard Newton, Lawrence T. Pileggi, Jan M. Rabaey, Alberto L. Sangiovanni-Vincentelli
Limitations and challenges of computer-aided design technology for CMOS VLSI. Proc. IEEE 89 (3) (2001)
Randal E. Bryant, Yirng-An Chen
Verification of arithmetic circuits using binary moment diagrams. Int. J. Softw. Tools Technol. Transf. 3 (2) (2001)
Yirng-An Chen, Randal E. Bryant
An efficient graph representation for arithmetic circuitverification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20 (12) (2001)
Miroslav N. Velev, Randal E. Bryant
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. DAC (2001)
Randal E. Bryant, Miroslav N. Velev
Boolean Satisfiability with Transitivity Constraints. CAV (2000)
Clayton B. McDonald, Randal E. Bryant
Symbolic timing simulation using cluster scheduling. DAC (2000)
Miroslav N. Velev, Randal E. Bryant
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. DAC (2000)
Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel
A Theory of Consistency for Modular Synchronous Systems. FMCAD (2000)
Chris Wilson, David L. Dill, Randal E. Bryant
Symbolic Simulation with Approximate Values. FMCAD (2000)
Randal E. Bryant, Miroslav N. Velev
Boolean Satisfiability with Transitivity Constraints CoRR (2000)
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)
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)
Randal E. Bryant, Steven M. German, Miroslav N. Velev
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. CAV (1999)
Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron
Optimizing Symbolic Model Checking for Constraint-Rich Models. CAV (1999)
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)
Miroslav N. Velev, Randal E. Bryant
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. DAC (1999)
Vishnu A. Patankar, Alok Jain, Randal E. Bryant
Formal Verification of an ARM Processor. VLSI Design (1999)
Clayton B. McDonald, Randal E. Bryant
Symbolic functional and timing verification of transistor-level circuits. ICCAD (1999)
Manish Pandey, Randal E. Bryant
Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 18 (7) (1999)
Miroslav N. Velev, Randal E. Bryant
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. TACAS (1998)
Miroslav N. Velev, Randal E. Bryant
Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. ICCD (1998)
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)
Miroslav N. Velev, Randal E. Bryant
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. ACSD (1998)
Yirng-An Chen, Randal E. Bryant
Verification of Floating-Point Adders. CAV (1998)

Randal E. Bryant.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Randal E. Bryant