B.Sc. (Honors), Stanford University (1989); Ph.D., Stanford University (1996); Member of the Research Staff, VLSI CAD Division, Fujitsu Laboratories of America (1995-1996); Assistant Professor, University of British Columbia (1996-2001); Assistant Professor, University of British Columbia (1996-2001); Associate Professor, (2001-2006); Full Professor, (2006-)
My main research interest is developing and applying automated formal verification techniques as a practical debugging tool for designing protocols, computer systems, software, and VLSI chips.
As the marketplace demands more features and higher performance delivered in shorter development times, traditional debugging and validation techniques are not keeping pace. Currently, large chip design projects spend more resources on validation than on design, and major projects in the future will likely require 2-3 validation engineers for each design engineer. Clearly, additional tools are needed to help debug designs.
Formal verification can help meet this need; especially promising are the new generation of automatic verification techniques. Note that my motivation is explicitly economic - find bugs faster and cheaper - rather than the more traditional use of formal verification to certify correctness. As a consequence, my research favors automation over mathematical expressiveness to minimize the labor invested in formal verification.
My research also emphasizes practical verification examples over theoretical results. I am, therefore, always on the lookout for real people working on complicated design projects, especially those involving complex protocols and concurrent processes. Although I have mainly focused on preliminary system-level and protocol-level verification, I'm happy to take a look at anything from gate-level circuits up to rough requirement specifications. Working on real problems drives the research in practical, useful directions, and research progress allows more complicated, interesting designs to be verified.
Jesse Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, and Zhichuan Zhang, ``Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values,'' Computer Aided Verification: Sixteenth International Conference (CAV), Lecture Notes in Computer Science Vol. 3114, pp. 427-439, Springer, 2004.
Jesse Bingham, and Alan J. Hu, ``Empirically Efficient Verification for a Class of Infinite-State Systems,'' Tools and Algorithms for the Construction and Analysis of Systems: 11th International Conference (TACAS), Lecture Notes in Computer Science Vol. 3440, pp. 77-92, Springer, 2005.
Xiushan Feng, and Alan J. Hu, ``Cutpoints for Formal Equivalence Verification of Embedded Software,'' 5th ACM International Conference on Embedded Software (EMSOFT), 2005, pp. 307-316.
Flavio M. de Paula, and Alan J. Hu, ``An Effective Guidance Strategy for Abstraction-Guided Simulation,'' 44th ACM/IEEE Design Automation Conference (DAC), pp. 63-68, 2007.
Domagoj Babic, and Alan J. Hu, ``Structural Abstraction of Software Verification Conditions,'' Computer Aided Verification: 19th International Conference (CAV), Lecture Notes in Computer Science Vol. 4590, pp. 366-378, Springer, 2007.