Alan Hu

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.