default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDRandal E. Bryant
Person information
- affiliation: Carnegie Mellon University, Pittsburgh, USA
- award (2007): IEEE Emanuel R. Piore Award
- award (1998): Paris Kanellakis Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[c112]Joseph E. Reeves
, Marijn J. H. Heule, Randal E. Bryant:
From Clauses to Klauses [inline-graphic not available: see fulltext]. CAV (1) 2024: 110-132- 2023
- [j37]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Preprocessing of Propagation Redundant Clauses. J. Autom. Reason. 67(3): 31 (2023) - [j36]Randal E. Bryant, Marijn J. H. Heule:
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. ACM Trans. Comput. Log. 24(4): 31:1-31:28 (2023) - [c111]Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule:
Certified Knowledge Compilation with Application to Verified Model Counting. SAT 2023: 6:1-6:20 - [i11]Mate Soos, Randal E. Bryant:
Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination. CoRR abs/2304.04292 (2023) - [i10]Randal E. Bryant:
Notes on "Bounds on BDD-Based Bucket Elimination". CoRR abs/2306.10337 (2023) - 2022
- [c110]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Preprocessing of Propagation Redundant Clauses. IJCAR 2022: 106-124 - [c109]Randal E. Bryant:
Tbuddy: A Proof-Generating BDD Package. FMCAD 2022: 49-58 - [c108]Randal E. Bryant, Armin Biere, Marijn J. H. Heule:
Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) 2022: 443-461 - [c107]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Moving Definition Variables in Quantified Boolean Formulas. TACAS (1) 2022: 462-479 - 2021
- [c106]Randal E. Bryant, Marijn J. H. Heule:
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. CADE 2021: 433-449 - [c105]Randal E. Bryant, Marijn J. H. Heule:
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. TACAS (1) 2021: 76-93 - [i9]Randal E. Bryant, Marijn J. H. Heule:
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. CoRR abs/2105.00885 (2021) - 2020
- [j35]Randal E. Bryant:
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. J. Autom. Reason. 64(7): 1361-1391 (2020) - [j34]Sankar Basu, Randal E. Bryant, Giovanni De Micheli, Thomas N. Theis, Lloyd Whitman:
Nonsilicon, Non-von Neumann Computing - Part II. Proc. IEEE 108(8): 1211-1218 (2020) - [i8]Randal E. Bryant, Randy H. Katz, Chase Hensel, Erwin P. Gianchandani:
From Data to Knowledge to Action: Enabling the Smart Grid. CoRR abs/2008.00055 (2020)
2010 – 2019
- 2019
- [j33]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): 11-18 (2019) - 2018
- [c104]Brian P. Railing, Randal E. Bryant:
Implementing Malloc: Students and Systems Programming. SIGCSE 2018: 104-109 - [c103]Randal E. Bryant:
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. TACAS (1) 2018: 81-98 - [p1]Randal E. Bryant:
Binary Decision Diagrams. Handbook of Model Checking 2018: 191-217 - 2017
- [c102]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: 262-291 - [i7]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 abs/1707.04352 (2017) - [i6]Randal E. Bryant:
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. CoRR abs/1710.06500 (2017) - 2016
- [c101]Randal E. Bryant:
EduPar 2016 Keynote. IPDPS Workshops 2016: 941 - 2014
- [j32]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): 72-75 (2014) - 2013
- [c100]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: 388-405 - 2011
- [j31]Randal E. Bryant:
Data-Intensive Scalable Computing for Scientific Applications. Comput. Sci. Eng. 13(6): 25-33 (2011) - [c99]Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia:
Learning conditional abstractions. FMCAD 2011: 116-124 - 2010
- [j30]Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi:
2009 CAV award announcement. Formal Methods Syst. Des. 36(3): 195-197 (2010) - [c98]Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, John W. O'Leary:
ATLAS: Automatic Term-level abstraction of RTL designs. MEMOCODE 2010: 31-40
2000 – 2009
- 2009
- [j29]Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi:
The 2008 CAV Award citation. Formal Methods Syst. Des. 35(1): 4-5 (2009) - [j28]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): 95-104 (2009) - 2008
- [j27]Rune Møller Jensen, Manuela M. Veloso, Randal E. Bryant:
State-set branching: Leveraging BDDs for heuristic search. Artif. Intell. 172(2-3): 103-139 (2008) - [c97]Randal E. Bryant:
A View from the Engine Room: Computational Support for Symbolic Model Checking. 25 Years of Model Checking 2008: 145-149 - 2007
- [j26]Sanjit A. Seshia, K. Subramani, Randal E. Bryant:
On Solving Boolean Combinations of UTVPI Constraints. J. Satisf. Boolean Model. Comput. 3(1-2): 67-90 (2007) - [j25]Shuvendu K. Lahiri, Randal E. Bryant:
Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. 9(1): 4 (2007) - [c96]Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady:
Deciding Bit-Vector Arithmetic with Abstraction. TACAS 2007: 358-372 - 2006
- [c95]Randal E. Bryant:
Formal Verification of Infinite State Systems Using Boolean Methods. LICS 2006: 3-4 - [c94]Randal E. Bryant:
Formal Verification of Infinite State Systems Using Boolean Methods. RTA 2006: 1-3 - 2005
- [j24]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): 134-149 (2005) - [j23]Sanjit A. Seshia, Randal E. Bryant:
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. Log. Methods Comput. Sci. 1(2) (2005) - [c93]Sanjit A. Seshia, Randal E. Bryant, Kenneth S. Stevens:
Modeling and Verifying Circuits Using Generalized Relative Timing. ASYNC 2005: 98-108 - [c92]Randal E. Bryant, Sanjit A. Seshia:
Decision Procedures Customized for Formal Verification. CADE 2005: 255-259 - [c91]Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant:
Automatic discovery of API-level exploits. ICSE 2005: 312-321 - [c90]Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Xiaodong Song, Randal E. Bryant:
Semantics-Aware Malware Detection. S&P 2005: 32-46 - [i5]Sanjit A. Seshia, Randal E. Bryant:
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. CoRR abs/cs/0508044 (2005) - 2004
- [c89]Rune Møller Jensen, Manuela M. Veloso, Randal E. Bryant:
Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic Non-Deterministic Planning. ICAPS 2004: 335-344 - [c88]Shuvendu K. Lahiri, Randal E. Bryant:
Indexed Predicate Discovery for Unbounded System Verification. CAV 2004: 135-147 - [c87]Amit Goel, Randal E. Bryant:
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. CAV 2004: 255-267 - [c86]Randal E. Bryant, Sriram K. Rajamani:
Verifying properties of hardware and software by predicate abstraction and model checking. ICCAD 2004: 437-438 - [c85]Sanjit A. Seshia, Randal E. Bryant:
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. LICS 2004: 100-109 - [c84]Randal E. Bryant:
System modeling and verification with UCLID. MEMOCODE 2004: 3-4 - [c83]Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur:
Revisiting Positive Equality. TACAS 2004: 1-15 - [c82]Shuvendu K. Lahiri, Randal E. Bryant:
Constructing Quantified Invariants via Predicate Abstraction. VMCAI 2004: 267-281 - [i4]Shuvendu K. Lahiri, Randal E. Bryant:
Predicate Abstraction with Indexed Predicates. CoRR cs.LO/0407006 (2004) - 2003
- [b1]Randal E. Bryant, David R. O'Hallaron:
Computer systems - a programmers perspective. Pearson Education 2003, ISBN 978-0-13-178456-7, pp. I-XXVIII, 1-978 - [j22]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): 73-106 (2003) - [c81]Rune Møller Jensen, Manuela M. Veloso, Randal E. Bryant:
Guided Symbolic Universal Planning. ICAPS 2003: 123-132 - [c80]Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook:
A Symbolic Approach to Predicate Abstraction. CAV 2003: 141-153 - [c79]Sanjit A. Seshia, Randal E. Bryant:
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. CAV 2003: 154-166 - [c78]Shuvendu K. Lahiri, Randal E. Bryant:
Deductive Verification of Advanced Out-of-Order Microprocessors. CAV 2003: 341-353 - [c77]Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia:
Convergence Testing in Term-Level Bounded Model Checking. CHARME 2003: 348-362 - [c76]Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant:
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. DAC 2003: 425-430 - [c75]Amit Goel, Gagan Hasteer, Randal E. Bryant:
Symbolic representation with ordered function templates. DAC 2003: 431-435 - [c74]Amit Goel, Randal E. Bryant:
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis. DATE 2003: 10816-10821 - [c73]Randal E. Bryant:
Reasoning about Infinite State Systems Using Boolean Methods. FSTTCS 2003: 399-407 - 2002
- [j21]Randal E. Bryant, Miroslav N. Velev:
Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3(4): 604-627 (2002) - [c72]Rune Møller Jensen, Randal E. Bryant, Manuela M. Veloso:
SetA*: An Efficient BDD-Based Heuristic Search Algorithm. AAAI/IAAI 2002: 668-673 - [c71]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: 78-92 - [c70]Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant:
Deciding Separation Formulas with SAT. CAV 2002: 209-222 - [c69]Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant:
Modeling and Verification of Out-of-Order Microprocessors in UCLID. FMCAD 2002: 142-159 - [i3]Randal E. Bryant, Christoph Meinel:
Ordered Binary Decision Diagrams in Electronic Design Automation. Universität Trier, Mathematik/Informatik, Forschungsbericht 02-20 (2002) - 2001
- [j20]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): 341-365 (2001) - [j19]Randal E. Bryant, Yirng-An Chen:
Verification of arithmetic circuits using binary moment diagrams. Int. J. Softw. Tools Technol. Transf. 3(2): 137-155 (2001) - [j18]Clayton B. McDonald, Randal E. Bryant:
CMOS circuit verification with symbolic switch-level timingsimulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20(3): 458-474 (2001) - [j17]Yirng-An Chen, Randal E. Bryant:
An efficient graph representation for arithmetic circuitverification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20(12): 1443-1454 (2001) - [j16]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): 93-134 (2001) - [c68]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: 235-240 - [c67]Miroslav N. Velev, Randal E. Bryant:
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. DAC 2001: 226-231 - [c66]Clayton B. McDonald, Randal E. Bryant:
Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis. DAC 2001: 283-288 - [c65]Clayton B. McDonald, Randal E. Bryant:
A Symbolic Simulation-Based Methodology for Generating Black-Box Timing Models of Custom Macrocells. ICCAD 2001: 501-506 - [c64]Randal E. Bryant, David R. O'Hallaron:
Introducing computer systems from a programmer's perspective. SIGCSE 2001: 90-94 - 2000
- [c63]Randal E. Bryant, Miroslav N. Velev:
Boolean Satisfiability with Transitivity Constraints. CAV 2000: 85-98 - [c62]Miroslav N. Velev, Randal E. Bryant:
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. DAC 2000: 112-117 - [c61]Clayton B. McDonald, Randal E. Bryant:
Symbolic timing simulation using cluster scheduling. DAC 2000: 254-259 - [c60]Chris Wilson, David L. Dill, Randal E. Bryant:
Symbolic Simulation with Approximate Values. FMCAD 2000: 470-485 - [c59]Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel:
A Theory of Consistency for Modular Synchronous Systems. FMCAD 2000: 486-504 - [i2]Randal E. Bryant, Miroslav N. Velev:
Boolean Satisfiability with Transitivity Constraints. CoRR cs.LO/0008001 (2000)
1990 – 1999
- 1999
- [j15]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): 918-935 (1999) - [c58]Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron:
Optimizing Symbolic Model Checking for Constraint-Rich Models. CAV 1999: 328-340 - [c57]Randal E. Bryant, Steven M. German, Miroslav N. Velev:
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. CAV 1999: 470-482 - [c56]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: 37-53 - [c55]Miroslav N. Velev, Randal E. Bryant:
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. DAC 1999: 397-401 - [c54]Clayton B. McDonald, Randal E. Bryant:
Symbolic functional and timing verification of transistor-level circuits. ICCAD 1999: 526-530 - [c53]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: 1-13 - [c52]Vishnu A. Patankar, Alok Jain, Randal E. Bryant:
Formal Verification of an ARM Processor. VLSI Design 1999: 282-287 - [i1]Randal E. Bryant, Steven M. German, Miroslav N. Velev:
Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic. CoRR cs.LO/9910014 (1999) - 1998
- [c51]Miroslav N. Velev, Randal E. Bryant:
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. ACSD 1998: 200-212 - [c50]Bwolen Yang, Yirng-An Chen, Randal E. Bryant, David R. O'Hallaron:
Space- and Time-Efficient BDD Construction via Working Set Control. ASP-DAC 1998: 423-432 - [c49]Yirng-An Chen, Randal E. Bryant:
Verification of Floating-Point Adders. CAV 1998: 488-499 - [c48]Randal E. Bryant, Gerry Musgrave:
User Experience with High Level Formal Verification (Panel). DAC 1998: 327 - [c47]Miroslav N. Velev, Randal E. Bryant:
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. FMCAD 1998: 18-35 - [c46]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: 255-289 - [c45]Miroslav N. Velev, Randal E. Bryant:
Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. ICCD 1998: 400-406 - [c44]Randal E. Bryant:
Formal Verification of Pipelined Processors. TACAS 1998: 1-4 - [c43]Miroslav N. Velev, Randal E. Bryant:
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. TACAS 1998: 136-150 - [e1]Basant R. Chawla, Randal E. Bryant, Jan M. Rabaey:
Proceedings of the 35th Conference on Design Automation, Moscone center, San Francico, California, USA, June 15-19, 1998. ACM Press 1998, ISBN 0-89791-964-5 [contents] - 1997
- [c42]Randal E. Bryant, Miroslav N. Velev:
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. ASIAN 1997: 18-31 - [c41]Manish Pandey, Randal E. Bryant:
Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. CAV 1997: 244-255 - [c40]Miroslav N. Velev, Randal E. Bryant, Alok Jain:
Efficient Modeling of Memory Arrays in Symbolic Simulation. CAV 1997: 388-399 - [c39]Kyle L. Nelson, Alok Jain, Randal E. Bryant:
Formal Verification of a Superscalar Execution Unit. DAC 1997: 161-166 - [c38]Manish Pandey, Richard Raimi, Randal E. Bryant, Magdy S. Abadir:
Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation. DAC 1997: 167-172 - [c37]Yirng-An Chen, Randal E. Bryant:
PHDD: an efficient graph representation for floating point circuit verification. ICCAD 1997: 2-7 - 1996
- [c36]Manish Pandey, Richard Raimi, Derek L. Beatty, Randal E. Bryant:
Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation. DAC 1996: 649-654 - [c35]Randal E. Bryant:
Bit-Level Analysis of an SRT Divider Circuit. DAC 1996: 661-665 - [c34]Alok Jain, Kyle L. Nelson, Randal E. Bryant:
Verifying Nondeterministic Implementations of Deterministic Systems. FMCAD 1996: 109-125 - [c33]Yirng-An Chen, Randal E. Bryant:
ACV: an arithmetic circuit verifier. ICCAD 1996: 361-365 - 1995
- [j14]Carl-Johan H. Seger, Randal E. Bryant:
Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Formal Methods Syst. Des. 6(2): 147-189 (1995) - [c32]Randal E. Bryant:
Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract). CAV 1995: 1-3 - [c31]