| Moving Definition Variables in Quantified Boolean Formulas | 0 | 0.34 | 2022 |
| Dual Proof Generation For Quantified Boolean Formulas With A Bdd-Based Solver | 0 | 0.34 | 2021 |
| Generating Extended Resolution Proofs with a BDD-Based SAT Solver. | 0 | 0.34 | 2021 |
| Nonsilicon, Non-von Neumann Computing - Part I [Scanning the Issue]. | 0 | 0.34 | 2019 |
| Implementing Malloc: Students and Systems Programming. | 0 | 0.34 | 2018 |
| Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. | 0 | 0.34 | 2018 |
| Parallel discrete event simulation: the making of a field | 1 | 0.35 | 2017 |
| Advances in Artificial Intelligence Require Progress Across all of Computer Science. | 0 | 0.34 | 2017 |
| Antisocial computing: exploring design risks in social computing systems | 2 | 0.41 | 2014 |
| Parrot: a practical runtime for deterministic, stable, and reliable threads | 42 | 1.13 | 2013 |
| Scalable Dynamic Partial Order Reduction. | 4 | 0.40 | 2012 |
| Learning conditional abstractions | 5 | 0.42 | 2011 |
| Data-Intensive Scalable Computing for Scientific Applications | 12 | 0.70 | 2011 |
| dBug: systematic testing of unmodified distributed and multi-threaded systems | 7 | 0.47 | 2011 |
| 2009 CAV award announcement | 0 | 0.34 | 2010 |
| dBug: systematic evaluation of distributed systems | 11 | 0.65 | 2010 |
| An abstraction-based decision procedure for bit-vector arithmetic | 12 | 0.70 | 2009 |
| State-set branching: Leveraging BDDs for heuristic search | 11 | 0.61 | 2008 |
| Decision procedures customized for formal verification | 0 | 0.34 | 2005 |
| Modeling and Verifying Circuits Using Generalized Relative Timing | 6 | 0.53 | 2005 |
| Tlsim And Evc: A Term-Level Symbolic Simulator And An Efficient Decision Procedure For The Logic Of Equality With Uninterpreted Functions And Memories | 22 | 0.69 | 2005 |
| Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds | 30 | 2.00 | 2005 |
| Automatic discovery of API-level exploits | 14 | 1.17 | 2005 |
| Semantics-Aware Malware Detection | 205 | 25.01 | 2005 |
| Verifying properties of hardware and software by predicate abstraction and model checking | 1 | 0.36 | 2004 |
| System modeling and verification with UCLID | 0 | 0.34 | 2004 |
| Constructing Quantified Invariants via Predicate Abstraction | 46 | 2.15 | 2004 |
| Predicate abstraction with indexed predicates | 27 | 1.03 | 2004 |
| Technical Program Committee | 0 | 0.34 | 2004 |
| Fault Tolerant Planning: Toward Probabilistic Uncertainty Models in Symbolic Non-Deterministic Planning | 16 | 0.71 | 2004 |
| Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis | 3 | 0.40 | 2003 |
| A hybrid SAT-based decision procedure for separation logic with uninterpreted functions | 50 | 2.58 | 2003 |
| Reasoning about Infinite State Systems Using Boolean Methods | 0 | 0.34 | 2003 |
| Guided Symbolic Universal Planning | 5 | 0.45 | 2003 |
| Symbolic representation with ordered function templates | 1 | 0.36 | 2003 |
| Modeling and Verification of Out-of-Order Microprocessors in UCLID | 57 | 2.49 | 2002 |
| SetA*: an efficient BDD-based heuristic search algorithm | 34 | 1.12 | 2002 |
| Deciding Separation Formulas with SAT | 48 | 3.05 | 2002 |
| An Efficient Graph Representation For Arithmetic Circuit Verification | 3 | 0.51 | 2001 |
| EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations | 10 | 0.69 | 2001 |
| Limitations and challenges of computer-aided design technology for CMOS VLSI | 31 | 3.74 | 2001 |
| Verification of arithmetic circuits using binary moment diagrams | 7 | 0.46 | 2001 |
| A Theory of Consistency for Modular Synchronous Systems | 5 | 0.96 | 2000 |
| Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction | 62 | 3.29 | 2000 |
| Boolean satisfiability with transitivity constraints | 55 | 3.96 | 2000 |
| Symbolic Simulation with Approximate Values | 14 | 0.77 | 2000 |
| Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions | 1 | 0.39 | 1999 |
| Optimizing Symbolic Model Checking for Constraint-Rich Models | 9 | 1.12 | 1999 |
| Symbolic functional and timing verification of transistor-level circuits | 7 | 0.81 | 1999 |
| Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions | 56 | 5.12 | 1999 |
