| 2024 | TACAS | 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 |
| 2022 | CLOUD | CoSpot: a cooperative VM allocation framework for increased revenue from spot instances. | Syed M. Iqbal, Haley Li, Shane Bergsma, Ivan Beschastnikh, Alan J. Hu |
| 2019 | CAV | 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, Neha Rungta, John Sizemore, Mark A. Stalzer, Preethi Srinivasan, Pavle Subotic, Carsten Varming, Blake Whaley |
| 2017 | IJCAI | Scalable Constraint-based Virtual Data Center Allocation. | Sam Bayless, Nodir Kodirov, Ivan Beschastnikh, Holger H. Hoos, Alan J. Hu |
| 2016 | CAV | Fast, Flexible, and Minimal CTL Synthesis via SMT. | Tobias Klenze, Sam Bayless, Alan J. Hu |
| 2016 | ICCAD | Scalable, high-quality, SAT-based multi-layer escape routing. | Sam Bayless, Holger H. Hoos, Alan J. Hu |
| 2015 | AAAI | SAT Modulo Monotonic Theories. | Sam Bayless, Noah Bayless, Holger H. Hoos, Alan J. Hu |
| 2015 | ICCAD | Reducing Post-Silicon Coverage Monitoring Overhead with Emulation and Bayesian Feature Selection. | Ricardo Ochoa Gallardo, Alan J. Hu, Andr Ivanov, Maryam S. Mirian |
| 2014 | DATE | Panel: Future SoC verification methodology: UVM evolution or revolution? | Rolf Drechsler, Christophe Chevallaz, Franco Fummi, Alan J. Hu, Ronny Morad, Frank Schirrmeister, Alex Goryachev |
| 2013 | FMCAD | Efficient modular SAT solving for IC3. | Sam Bayless, Celina G. Val, Thomas Ball, Holger H. Hoos, Alan J. Hu |
| 2012 | CAV | nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces. | Flavio M. de Paula, Alan J. Hu, Amir Nahir |
| 2012 | SAT | Single-Solver Algorithms for 2QBF - (Poster Presentation). | Sam Bayless, Alan J. Hu |
| 2011 | DAC | 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 |
| 2011 | DNA | Less Haste, Less Waste: On Recycling and Its Limits in Strand Displacement Systems. | Anne Condon, Alan J. Hu, Jn Manuch, Chris Thachuk |
| 2010 | DAC | 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 |
| 2009 | VMCAI | A Scalable Memory Model for Low-Level Code. | Zvonimir Rakamaric, Alan J. Hu |
| 2008 | FMCAD | BackSpace: Formal Analysis for Post-Silicon Debug. | Flavio M. de Paula, Marcel Gort, Alan J. Hu, Steven J. E. Wilton, Jin Yang |
| 2008 | ICSE | Calysto: scalable and precise extended static checking. | Domagoj Babic, Alan J. Hu |
| 2007 | ATVA | Verifying Heap-Manipulating Programs in an SMT Framework. | Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti |
| 2007 | CAV | Structural Abstraction of Software Verification Conditions. | Domagoj Babic, Alan J. Hu |
| 2007 | DAC | Verification Coverage: When is Enough, Enough? | Francine Bacchini, Alan J. Hu, Tom Fitzpatrick, Rajeev Ranjan, David Lacey, Mercedes Tan, Andrew Piziali, Avi Ziv |
| 2007 | DAC | An Effective Guidance Strategy for Abstraction-Guided Simulation. | Flavio M. de Paula, Alan J. Hu |
| 2007 | FMCAD | Boosting Verification by Automatic Tuning of Decision Procedures. | Frank Hutter, Domagoj Babic, Holger H. Hoos, Alan J. Hu |
| 2007 | SEFM | Proving Termination by Divergence. | Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook |
| 2007 | VMCAI | 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 |
| 2006 | CAV | EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation. | Flavio M. de Paula, Alan J. Hu |
| 2006 | DAC | Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification. | Xiushan Feng, Alan J. Hu |
| 2005 | ASPDAC | Integration of supercubing and learning in a SAT solver. | Domagoj Babic, Alan J. Hu |
| 2005 | ASPDAC | Partitioned model checking from software specifications. | Xiushan Feng, Alan J. Hu, Jin Yang |
| 2005 | DAC | Efficient SAT solving: beyond supercubes. | Domagoj Babic, Jesse D. Bingham, Alan J. Hu |
| 2005 | EMSOFT | Cutpoints for formal equivalence verification of embedded software. | Xiushan Feng, Alan J. Hu |
| 2005 | HPCA | 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 |
| 2005 | TACAS | Empirically Efficient Verification for a Class of Infinite-State Systems. | Jesse D. Bingham, Alan J. Hu |
| 2004 | CAV | Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values. | Jesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, Zhichuan Zhang |
| 2004 | ICCD | Generating Monitor Circuits for Simulation-Friendly GSTE Assertion Graphs. | Kelvin Ng, Alan J. Hu, Jin Yang |
| 2003 | ICCAD | Efficient Generation of Monitor Circuits for GSTE Assertion Graphs. | Alan J. Hu, Jeremy Casas, Jin Yang |
| 2003 | SPAA | Toward a decidable notion of sequential consistency. | Jesse D. Bingham, Anne Condon, Alan J. Hu |
| 2002 | CAV | Semi-formal Bounded Model Checking. | Jesse D. Bingham, Alan J. Hu |
| 2002 | DAC | High-Level specification and automatic generation of IP interface monitors. | Marcio T. Oliveira, Alan J. Hu |
| 2001 | ICCD | Fast Specification of Cycle-accurate Processor Models. | Felix Sheng-Ho Chang, Alan J. Hu |
| 2001 | SPAA | Automatable verification of sequential consistency. | Anne Condon, Alan J. Hu |
| 2000 | DAC | Automatic formal verification of DSP software. | David W. Currie, Alan J. Hu, Sreeranga P. Rajan |
| 2000 | FMCAD | Monitor-Based Formal Specification of PCI. | Kanna Shimizu, David L. Dill, Alan J. Hu |
| 2000 | ICCD | Source-Level Transformations for Improved Formal Verification. | Brian D. Winters, Alan J. Hu |
| 1999 | FORTE | Model-Checking a Secure Gorup Communication Protocol: A Case Study. | Alan J. Hu, Rui Li, Xizheng Shi, Son T. Vuong |
| 1999 | UAI | SPUDD: Stochastic Planning using Decision Diagrams. | Jesse Hoey, Robert St-Aubin, Alan J. Hu, Craig Boutilier |
| 1998 | DAC | Approximate Reachability with BDDs Using Overlapping Projections. | Shankar G. Govindaraju, David L. Dill, Alan J. Hu, Mark Horowitz |
| 1998 | FM | Two Real Formal Verification Experiences: ATM Switch Chip and Parallel Cache Protocol. | Masahiro Fujita, Sreeranga P. Rajan, Alan J. Hu |
| 1998 | FMCAD | BDDNOW: A Parallel BDD Package. | Kim Milvang-Jensen, Alan J. Hu |
| 1997 | ICCD | Formal Verification of the HAL S1 System Cache Coherence Protocol. | Alan J. Hu, Masahiro Fujita, Chris Wilson |
| 1994 | DAC | New Techniques for Efficient Verification with Implicitly Conjoined BDDs. | Alan J. Hu, Gary York, David L. Dill |
| 1993 | CAV | Efficient Verification with BDDs using Implicitly Conjoined Invariants. | Alan J. Hu, David L. Dill |
| 1993 | DAC | Reducing BDD Size by Exploiting Functional Dependencies. | Alan J. Hu, David L. Dill |
| 1992 | CAV | Higher-Level Specification and Verification with BDDs. | Alan J. Hu, David L. Dill, Andreas J. Drexler, C. Han Yang |
| 1992 | ICCD | Protocol Verification as a Hardware Design Aid. | David L. Dill, Andreas J. Drexler, Alan J. Hu, C. Han Yang |
| 1991 | CAV | Checking for Language Inclusion Using Simulation Preorders. | David L. Dill, Alan J. Hu, Howard Wong-Toi |