Selection of the optimum uniform partition search. - Alan J. Hu (Computing, 1986)

Checking for Language Inclusion Using Simulation Preorders. - David L. Dill; Alan J. Hu; Howard Wong-Toi (CAV, 1991)

Higher-Level Specification and Verification with BDDs. - Alan J. Hu; David L. Dill; Andreas J. Drexler; C. Han Yang (CAV, 1992)

Protocol Verification as a Hardware Design Aid. - David L. Dill; Andreas J. Drexler; Alan J. Hu; C. Han Yang (ICCD, 1992)

Efficient Verification with BDDs using Implicitly Conjoined Invariants. - Alan J. Hu; David L. Dill (CAV, 1993)

Reducing BDD Size by Exploiting Functional Dependencies. - Alan J. Hu; David L. Dill (DAC, 1993)

New Techniques for Efficient Verification with Implicitly Conjoined BDDs. - Alan J. Hu; Gary York; David L. Dill (DAC, 1994)

Formal Verification of the HAL S1 System Cache Coherence Protocol. - Alan J. Hu; Masahiro Fujita; Chris Wilson (ICCD, 1997)

Approximate Reachability with BDDs Using Overlapping Projections. - Shankar G. Govindaraju; David L. Dill; Alan J. Hu; Mark Horowitz (DAC, 1998)

Two Real Formal Verification Experiences: ATM Switch Chip and Parallel Cache Protocol. - Masahiro Fujita; Sreeranga P. Rajan; Alan J. Hu (FM-Trends, 1998)

BDDNOW: A Parallel BDD Package. - Kim Milvang-Jensen; Alan J. Hu (FMCAD, 1998)

Model-Checking a Secure Gorup Communication Protocol: A Case Study. - Alan J. Hu; Rui Li; Xizheng Shi; Son T. Vuong (FORTE, 1999)

SPUDD: Stochastic Planning using Decision Diagrams. - Jesse Hoey; Robert St-Aubin; Alan J. Hu; Craig Boutilier (UAI, 1999)

Automatic formal verification of DSP software. - David W. Currie; Alan J. Hu; Sreeranga P. Rajan (DAC, 2000)

Monitor-Based Formal Specification of PCI. - Kanna Shimizu; David L. Dill; Alan J. Hu (FMCAD, 2000)

Source-Level Transformations for Improved Formal Verification. - Brian D. Winters; Alan J. Hu (ICCD, 2000)

Register Transformations with Multiple Clock Domains. - Alvin R. Albrecht; Alan J. Hu (CHARME, 2001)

Proving sequential consistency by model checking. - Tim Braun; Anne Condon; Alan J. Hu; Kai S. Juse; Marius Laza; Michael Leslie; Rita Sharma (HLDVT, 2001)

Fast Specification of Cycle-accurate Processor Models. - Felix Sheng-Ho Chang; Alan J. Hu (ICCD, 2001)

Automatable verification of sequential consistency. - Anne Condon; Alan J. Hu (SPAA, 2001)

Semi-formal Bounded Model Checking. - Jesse D. Bingham; Alan J. Hu (CAV, 2002)

High-Level specification and automatic generation of IP interface monitors. - Marcio T. Oliveira; Alan J. Hu (DAC, 2002)

Automatic formal verification for scheduled VLIW code. - Xiushan Feng; Alan J. Hu (LCTES-SCOPES, 2002)

Reasoning about GSTE Assertion Graphs. - Alan J. Hu; Jeremy Casas; Jin Yang 006 (CHARME, 2003)

Efficient Generation of Monitor Circuits for GSTE Assertion Graphs. - Alan J. Hu; Jeremy Casas; Jin Yang (ICCAD, 2003)

Toward a decidable notion of sequential consistency. - Jesse D. Bingham; Anne Condon; Alan J. Hu (SPAA, 2003)

Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values. - Jesse D. Bingham; Anne Condon; Alan J. Hu; Shaz Qadeer; Zhichuan Zhang (CAV, 2004)

Generating Monitor Circuits for Simulation-Friendly GSTE Assertion Graphs. - Kelvin Ng; Alan J. Hu; Jin Yang (ICCD, 2004)

Fixing Races for Fun and Profit: How to Use access(2). - Drew Dean; Alan J. Hu (USENIX Security Symposium, 2004)

Integration of supercubing and learning in a SAT solver. - Domagoj Babic; Alan J. Hu (ASP-DAC, 2005)

Partitioned model checking from software specifications. - Xiushan Feng; Alan J. Hu; Jin Yang 006 (ASP-DAC, 2005)

Efficient SAT solving: beyond supercubes. - Domagoj Babic; Jesse D. Bingham; Alan J. Hu (DAC, 2005)

Cutpoints for formal equivalence verification of embedded software. - Xiushan Feng; Alan J. Hu (EMSOFT, 2005)

B-cubing theory: new possibilities for efficient SAT-solving. - Domagoj Babic; Jesse D. Bingham; Alan J. Hu (HLDVT, 2005)

Improving Multiple-CMP Systems Using Token Coherence. - Michael R. Marty; Jesse D. Bingham; Mark D. Hill; Alan J. Hu; Milo M. K. Martin; David A. Wood 001 (HPCA, 2005)

Empirically Efficient Verification for a Class of Infinite-State Systems. - Jesse D. Bingham; Alan J. Hu (TACAS, 2005)

EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation. - Flavio M. de Paula; Alan J. Hu (CAV, 2006)

Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification. - Xiushan Feng; Alan J. Hu (DAC, 2006)

EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation. - Alan J. Hu (HLDVT, 2006)

Panel: Assertion-Based Verification -What's the Big Deal? - Sandeep K. Shukla; Alan J. Hu; Jacob Abrahams; Pranav Ashar; Harry Foster; Avner Landver; Carl Pixley (HLDVT, 2006)

Embedded Software Verification Using Symbolic Execution and Uninterpreted Functions. - David W. Currie; Xiushan Feng; Masahiro Fujita; Alan J. Hu; Mark Kwan; Sreeranga P. Rajan (Int. J. Parallel Program., 2006)

System-on-Chip: Reuse and Integration. - Resve A. Saleh; Steven J. E. Wilton; Shahriar Mirabbasi; Alan J. Hu; Mark R. Greenstreet; Guy Lemieux; Partha Pratim Pande; Cristian Grecu; André Ivanov (Proc. IEEE, 2006)

B-Cubing: New Possibilities for Efficient SAT-Solving. - Domagoj Babic; Jesse D. Bingham; Alan J. Hu (IEEE Trans. Computers, 2006)

Verifying Heap-Manipulating Programs in an SMT Framework. - Zvonimir Rakamaric; Roberto Bruttomesso; Alan J. Hu; Alessandro Cimatti (ATVA, 2007)

Structural Abstraction of Software Verification Conditions. - Domagoj Babic; Alan J. Hu (CAV, 2007)

Verification Coverage: When is Enough, Enough? - Francine Bacchini; Alan J. Hu; Tom Fitzpatrick; Rajeev Ranjan; David Lacey; Mercedes Tan; Andrew Piziali; Avi Ziv (DAC, 2007)

An Effective Guidance Strategy for Abstraction-Guided Simulation. - Flavio M. de Paula; Alan J. Hu (DAC, 2007)

Boosting Verification by Automatic Tuning of Decision Procedures. - Frank Hutter; Domagoj Babic; Holger H. Hoos; Alan J. Hu (FMCAD, 2007)

Exploiting Shared Structure in Software Verification Conditions. - Domagoj Babic; Alan J. Hu (Haifa Verification Conference, 2007)

Simulation vs. Formal: Absorb What Is Useful; Reject What Is Useless. - Alan J. Hu (Haifa Verification Conference, 2007)

Proving Termination by Divergence. - Domagoj Babic; Alan J. Hu; Zvonimir Rakamaric; Byron Cook (SEFM, 2007)

An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures. - Zvonimir Rakamaric; Jesse D. Bingham; Alan J. Hu (VMCAI, 2007)

BackSpace: Formal Analysis for Post-Silicon Debug. - Flavio M. de Paula; Marcel Gort; Alan J. Hu; Steven J. E. Wilton; Jin Yang 006 (FMCAD, 2008)

Calysto: scalable and precise extended static checking. - Domagoj Babic; Alan J. Hu (ICSE, 2008)

Automatic Inference of Frame Axioms Using Static Analysis. - Zvonimir Rakamaric; Alan J. Hu (ASE, 2008)

BackSpace: Moving Towards Reality. - Flavio M. de Paula; Marcel Gort; Alan J. Hu; Steven J. E. Wilton (MTV, 2008)

A Scalable Memory Model for Low-Level Code. - Zvonimir Rakamaric; Alan J. Hu (VMCAI, 2009)

Approximating the safely reusable set of learned facts. - Domagoj Babic; Alan J. Hu (Int. J. Softw. Tools Technol. Transf., 2009)

Bridging pre-silicon verification and post-silicon validation. - Amir Nahir; Avi Ziv; Rajesh Galivanche; Alan J. Hu; Miron Abramovici; Albert Camilleri; Bob Bentley; Harry Foster; Valeria Bertacco; Shakti Kapoor (DAC, 2010)

Special Session on Debugging. - Yoav Hollander; Alan J. Hu; João Lourenço; Ronny Morad (Haifa Verification Conference, 2010)

Context-Bounded Translations for Concurrent Software: An Empirical Evaluation. - Naghmeh Ghafari; Alan J. Hu; Zvonimir Rakamaric (SPIN, 2010)

TAB-BackSpace: unlimited-length trace buffers with zero additional on-chip overhead. - Flavio M. de Paula; Amir Nahir; Ziv Nevo; Avigail Orni; Alan J. Hu (DAC, 2011)

Less Haste, Less Waste: On Recycling and Its Limits in Strand Displacement Systems. - Anne Condon; Alan J. Hu; Ján Manuch; Chris Thachuk (DNA, 2011)

Post-silicon code coverage evaluation with reduced area overhead for functional verification of SoC. - Mehdi Karimibiuki; Kyle Balston; Alan J. Hu; André Ivanov (HLDVT, 2011)

Preface. - Hana Chockler; Alan J. Hu (Int. J. Softw. Tools Technol. Transf., 2011)

nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces. - Flavio M. de Paula; Alan J. Hu; Amir Nahir (CAV, 2012)

Lazy suspect-set computation: fault diagnosis for deep electrical bugs. - Dipanjan Sengupta; Flavio M. de Paula; Alan J. Hu; Andreas G. Veneris; André Ivanov (ACM Great Lakes Symposium on VLSI, 2012)

Emulation in post-silicon validation: It's not just for functionality anymore. - Kyle Balston; Alan J. Hu; Steven J. E. Wilton; Amir Nahir (HLDVT, 2012)

Single-Solver Algorithms for 2QBF - (Poster Presentation). - Sam Bayless; Alan J. Hu (SAT, 2012)

Formal-Analysis-Based Trace Computation for Post-Silicon Debug. - Marcel Gort; Flavio M. de Paula; Johnny J. W. Kuan; Tor M. Aamodt; Alan J. Hu; Steven J. E. Wilton; Jin Yang 006 (IEEE Trans. Very Large Scale Integr. Syst., 2012)

Efficient modular SAT solving for IC3. - Sam Bayless; Celina G. Val; Thomas Ball 001; Holger H. Hoos; Alan J. Hu (FMCAD, 2013)

Proving termination of nonlinear command sequences. - Domagoj Babic; Byron Cook; Alan J. Hu; Zvonimir Rakamaric (Formal Aspects Comput., 2013)

Post-Silicon Code Coverage for Multiprocessor System-on-Chip Designs. - Kyle Balston; Mehdi Karimibiuki; Alan J. Hu; André Ivanov; Steven J. E. Wilton (IEEE Trans. Computers, 2013)

Panel: Future SoC verification methodology: UVM evolution or revolution? - Rolf Drechsler; Christophe Chevallaz; Franco Fummi; Alan J. Hu; Ronny Morad; Frank Schirrmeister; Alex Goryachev (DATE, 2014)

Efficient Coverage-Driven Stimulus Generation Using Simultaneous SAT Solving, with Application to SystemVerilog. - An-Che Cheng; Chia-Chih Jack Yen; Celina G. Val; Sam Bayless; Alan J. Hu; Iris Hui-Ru Jiang; Jing-Yang Jou (ACM Trans. Design Autom. Electr. Syst., 2014)

SAT Modulo Monotonic Theories. - Sam Bayless; Noah Bayless; Holger H. Hoos; Alan J. Hu (AAAI, 2015)

Reducing Post-Silicon Coverage Monitoring Overhead with Emulation and Bayesian Feature Selection. - Ricardo Ochoa Gallardo; Alan J. Hu; André Ivanov; Maryam S. Mirian (ICCAD, 2015)

Fast, Flexible, and Minimal CTL Synthesis via SMT. - Tobias Klenze; Sam Bayless; Alan J. Hu (CAV (1), 2016)

Precisely Measuring Quantitative Information Flow: 10K Lines of Code and Beyond. - Celina G. Val; Michael A. Enescu; Sam Bayless; William Aiello; Alan J. Hu (EuroS&P, 2016)

Scalable, high-quality, SAT-based multi-layer escape routing. - Sam Bayless; Holger H. Hoos; Alan J. Hu (ICCAD, 2016)

Scalable Constraint-based Virtual Data Center Allocation. - Sam Bayless; Nodir Kodirov; Ivan Beschastnikh; Holger H. Hoos; Alan J. Hu (IJCAI, 2017)

VNF chain allocation and management at data center scale. - Nodir Kodirov; Sam Bayless; Fabian Ruffy; Ivan Beschastnikh; Holger H. Hoos; Alan J. Hu (ANCS, 2018)

VNF chain abstraction for cloud service providers. - Nodir Kodirov; Sam Bayless; Fabian Ruffy; Ivan Beschastnikh; Holger H. Hoos; Alan J. Hu (ANCS, 2018)

Reachability Analysis for AWS-Based Networks. - John Backes; Sam Bayless; Byron Cook; Catherine Dodge; Andrew Gacek; Alan J. Hu; Temesghen Kahsai; Bill Kocik; Evgenii Kotelnikov; Jure Kukovec; Sean McLaughlin; Jason Reed 004; et al. (CAV (2), 2019)

Scalable constraint-based virtual data center allocation. - Sam Bayless; Nodir Kodirov; Syed M. Iqbal; Ivan Beschastnikh; Holger H. Hoos; Alan J. Hu (Artif. Intell., 2020)

Cache abstraction for data race detection in heterogeneous systems with non-coherent accelerators. - May Young; Alan J. Hu; Guy G. F. Lemieux (LCTES, 2021)

CoSpot: a cooperative VM allocation framework for increased revenue from spot instances. - Syed M. Iqbal; Haley Li; Shane Bergsma; Ivan Beschastnikh; Alan J. Hu (SoCC, 2022)

Gridiron: A Technique for Augmenting Cloud Workloads with Network Bandwidth Requirements. - Nodir Kodirov; Shane Bergsma; Syed M. Iqbal; Alan J. Hu; Ivan Beschastnikh; Margo I. Seltzer (CoRR, 2022)

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories. - Nick Feng; Alan J. Hu; Sam Bayless; Syed M. Iqbal; Patrick Trentin; Mike Whalen; Lee Pike; John Backes (TACAS (1), 2024)