| 2026 | SAT | Factoring Learned Clauses. | Florian Pollitt, Zachary Battleman, Mathias Fleury, Yakir Vizel, Marijn J. H. Heule, Armin Biere, Randal E. Bryant |
| 2025 | SAT | Certifying Projected Knowledge Compilation. | Randal E. Bryant, Yong Kiam Tan, Marijn J. H. Heule |
| 2024 | CAV | From Clauses to Klauses. | Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant |
| 2024 | FMCAD | Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs. | Karthik V. Nukala, Soumyaditya Choudhuri, Randal E. Bryant, Marijn J. H. Heule |
| 2023 | SAT | Certified Knowledge Compilation with Application to Verified Model Counting. | Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule |
| 2022 | CADE | Preprocessing of Propagation Redundant Clauses. | Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant |
| 2022 | FMCAD | Tbuddy: A Proof-Generating BDD Package. | Randal E. Bryant |
| 2022 | TACAS | Clausal Proofs for Pseudo-Boolean Reasoning. | Randal E. Bryant, Armin Biere, Marijn J. H. Heule |
| 2022 | TACAS | Moving Definition Variables in Quantified Boolean Formulas. | Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant |
| 2021 | CADE | Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. | Randal E. Bryant, Marijn J. H. Heule |
| 2021 | TACAS | Generating Extended Resolution Proofs with a BDD-Based SAT Solver. | Randal E. Bryant, Marijn J. H. Heule |
| 2018 | SIGCSE | Implementing Malloc: Students and Systems Programming. | Brian P. Railing, Randal E. Bryant |
| 2018 | TACAS | Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. | Randal E. Bryant |
| 2017 | WSC | Parallel discrete event simulation: The making of a field. | Richard M. Fujimoto, Rajive L. Bagrodia, Randal E. Bryant, K. Mani Chandy, David R. Jefferson, Jayadev Misra, David M. Nicol, Brian W. Unger |
| 2013 | SOSP | Parrot: a practical runtime for deterministic, stable, and reliable threads. | Heming Cui, Jir Simsa, Yi-Hong Lin, Hao Li, Ben Blum, Xinan Xu, Junfeng Yang, Garth A. Gibson, Randal E. Bryant |
| 2011 | FMCAD | Learning conditional abstractions. | Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia |
| 2010 | MEMOCODE | ATLAS: Automatic Term-level abstraction of RTL designs. | Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, John W. O'Leary |
| 2007 | TACAS | Deciding Bit-Vector Arithmetic with Abstraction. | Randal E. Bryant, Daniel Kroening, Jol Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady |
| 2006 | LICS | Formal Verification of Infinite State Systems Using Boolean Methods. | Randal E. Bryant |
| 2005 | CADE | Decision Procedures Customized for Formal Verification. | Randal E. Bryant, Sanjit A. Seshia |
| 2005 | ICSE | Automatic discovery of API-level exploits. | Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant |
| 2005 | SP | Semantics-Aware Malware Detection. | Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Xiaodong Song, Randal E. Bryant |
| 2004 | CAV | Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. | Amit Goel, Randal E. Bryant |
| 2004 | CAV | Indexed Predicate Discovery for Unbounded System Verification. | Shuvendu K. Lahiri, Randal E. Bryant |
| 2004 | ICCAD | Verifying properties of hardware and software by predicate abstraction and model checking. | Randal E. Bryant, Sriram K. Rajamani |
| 2004 | LICS | Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. | Sanjit A. Seshia, Randal E. Bryant |
| 2004 | MEMOCODE | System modeling and verification with UCLID. | Randal E. Bryant |
| 2004 | TACAS | Revisiting Positive Equality. | Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur |
| 2004 | VMCAI | Constructing Quantified Invariants via Predicate Abstraction. | Shuvendu K. Lahiri, Randal E. Bryant |
| 2003 | CAV | Deductive Verification of Advanced Out-of-Order Microprocessors. | Shuvendu K. Lahiri, Randal E. Bryant |
| 2003 | CAV | A Symbolic Approach to Predicate Abstraction. | Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook |
| 2003 | CAV | Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. | Sanjit A. Seshia, Randal E. Bryant |
| 2003 | DAC | Symbolic representation with ordered function templates. | Amit Goel, Gagan Hasteer, Randal E. Bryant |
| 2003 | DAC | A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. | Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant |
| 2003 | DATE | Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis. | Amit Goel, Randal E. Bryant |
| 2002 | AAAI | SetA*: An Efficient BDD-Based Heuristic Search Algorithm. | Rune Mller Jensen, Randal E. Bryant, Manuela M. Veloso |
| 2002 | CAV | Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. | Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia |
| 2002 | CAV | Deciding Separation Formulas with SAT. | Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant |
| 2002 | FMCAD | Modeling and Verification of Out-of-Order Microprocessors in UCLID. | Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant |
| 2001 | CAV | EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. | Miroslav N. Velev, Randal E. Bryant |
| 2001 | DAC | Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis. | Clayton B. McDonald, Randal E. Bryant |
| 2001 | DAC | Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. | Miroslav N. Velev, Randal E. Bryant |
| 2001 | ICCAD | A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells. | Clayton B. McDonald, Randal E. Bryant |
| 2001 | SIGCSE | Introducing computer systems from a programmer's perspective. | Randal E. Bryant, David R. O'Hallaron |
| 2000 | CAV | Boolean Satisfiability with Transitivity Constraints. | Randal E. Bryant, Miroslav N. Velev |
| 2000 | DAC | Symbolic timing simulation using cluster scheduling. | Clayton B. McDonald, Randal E. Bryant |
| 2000 | DAC | Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. | Miroslav N. Velev, Randal E. Bryant |
| 2000 | FMCAD | A Theory of Consistency for Modular Synchronous Systems. | Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel |
| 2000 | FMCAD | Symbolic Simulation with Approximate Values. | Chris Wilson, David L. Dill, Randal E. Bryant |
| 1999 | CAV | Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
| 1999 | CAV | Optimizing Symbolic Model Checking for Constraint-Rich Models. | Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron |
| 1999 | DAC | Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. | Miroslav N. Velev, Randal E. Bryant |
| 1999 | ICCAD | Symbolic functional and timing verification of transistor-level circuits. | Clayton B. McDonald, Randal E. Bryant |
| 1999 | VLSID | Formal Verification of an ARM Processor. | Vishnu A. Patankar, Alok Jain, Randal E. Bryant |
| 1999 | TABLEAUX | Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
| 1998 | ASPDAC | Space- and Time-Efficient BDD Construction via Working Set Control. | Bwolen Yang, Yirng-An Chen, Randal E. Bryant, David R. O'Hallaron |
| 1998 | CAV | Verification of Floating-Point Adders. | Yirng-An Chen, Randal E. Bryant |
| 1998 | DAC | User Experience with High Level Formal Verification (Panel). | Randal E. Bryant, Gerry Musgrave |
| 1998 | FMCAD | Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. | Miroslav N. Velev, Randal E. Bryant |
| 1998 | FMCAD | A Performance Study of BDD-Based Model Checking. | Bwolen Yang, Randal E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, Fabio Somenzi |
| 1998 | ICCD | Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. | Miroslav N. Velev, Randal E. Bryant |
| 1998 | TACAS | Formal Verification of Pipelined Processors. | Randal E. Bryant |
| 1998 | TACAS | Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. | Miroslav N. Velev, Randal E. Bryant |
| 1997 | CAV | Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. | Manish Pandey, Randal E. Bryant |
| 1997 | CAV | Efficient Modeling of Memory Arrays in Symbolic Simulation. | Miroslav N. Velev, Randal E. Bryant, Alok Jain |
| 1997 | DAC | Formal Verification of a Superscalar Execution Unit. | Kyle L. Nelson, Alok Jain, Randal E. Bryant |
| 1997 | DAC | Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation. | Manish Pandey, Richard Raimi, Randal E. Bryant, Magdy S. Abadir |
| 1997 | ICCAD | PHDD: an efficient graph representation for floating point circuit verification. | Yirng-An Chen, Randal E. Bryant |
| 1996 | DAC | Bit-Level Analysis of an SRT Divider Circuit. | Randal E. Bryant |
| 1996 | DAC | Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation. | Manish Pandey, Richard Raimi, Derek L. Beatty, Randal E. Bryant |
| 1996 | FMCAD | Verifying Nondeterministic Implementations of Deterministic Systems. | Alok Jain, Kyle L. Nelson, Randal E. Bryant |
| 1996 | ICCAD | ACV: an arithmetic circuit verifier. | Yirng-An Chen, Randal E. Bryant |
| 1995 | CAV | Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract). | Randal E. Bryant |
| 1995 | DAC | Verification of Arithmetic Circuits with Binary Moment Diagrams. | Randal E. Bryant, Yirng-An Chen |
| 1995 | DAC | Automatic Clock Abstraction from Sequential Circuits. | Samir Jain, Randal E. Bryant, Alok Jain |
| 1995 | ICCAD | Binary decision diagrams and beyond: enabling technologies for formal verification. | Randal E. Bryant |
| 1995 | ICCD | Extraction of finite state machines from transistor netlists by symbolic simulation. | Manish Pandey, Alok Jain, Randal E. Bryant, Derek L. Beatty, Gary York, Samir Jain |
| 1994 | DAC | Formally Verifying a Microprocessor Using a Simulation Methodology. | Derek L. Beatty, Randal E. Bryant |
| 1993 | ICCAD | Inverter minimization in multi-level logic networks. | Alok Jain, Randal E. Bryant |
| 1993 | ICCD | Symbolic Analysis Methods for Masks, Circuits, and Systems. | Randal E. Bryant |
| 1993 | ICPP | An Analysis of Hashing on Parallel and Vector Computers. | Thomas J. Sheffler, Randal E. Bryant |
| 1993 | ISCAS | Geometric characterization of series-parallel variable resistor networks. | Randal E. Bryant, J. D. Tygar, Lawrence P. Huang |
| 1991 | DAC | Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation. | Randal E. Bryant, Derek L. Beatty, Carl-Johan H. Seger |
| 1991 | DAC | Mapping Switch-Level Simulation onto Gate-Level Hardware Accelerators. | Alok Jain, Randal E. Bryant |
| 1991 | ICCAD | Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis. | Randal E. Bryant |
| 1990 | CAV | Formal Verification of Digital Circuits Using Symbolic Ternary System Models. | Randal E. Bryant, Carl-Johan H. Seger |
| 1990 | DAC | Efficient Implementation of a BDD Package. | Karl S. Brace, Richard L. Rudell, Randal E. Bryant |
| 1990 | DAC | Symbolic Simulation - Techniques and Applications. | Randal E. Bryant |
| 1989 | DAC | Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation. | Kyeongsoon Cho, Randal E. Bryant |
| 1989 | DAC | Massively Parallel Switch-Level Simulation: A Feasibility Study. | Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar |
| 1989 | ISCA | Logic Simulation on Massively Parallel Architectures. | Saul A. Kravitz, Randal E. Bryant, Rob A. Rutenbar |
| 1988 | DAC | Fast Incremental Circuit Analysis Using Extracted Hierarchy. | Derek L. Beatty, Randal E. Bryant |
| 1988 | DAC | CAD Tool Needs for System Designers. | Randal E. Bryant |
| 1988 | ICCAD | Data parallel switch-level simulation. | Randal E. Bryant |
| 1987 | DAC | COSMOS: A Compiled Simulator for MOS Circuits. | Randal E. Bryant, Derek L. Beatty, Karl S. Brace, Kyeongsoon Cho, Thomas J. Sheffler |
| 1985 | DAC | Symbolic manipulation of Boolean functions using a graphical representation. | Randal E. Bryant |
| 1985 | DAC | Performance evaluation of FMOSSIM, a concurrent switch-level fault simulator. | Randal E. Bryant, Michael Dd. Schuster |
| 1981 | DAC | MOSSIM: A switch-level simulator for MOS LSI. | Randal E. Bryant |