Ensuring design correctness is crucial in all hardware and software designs. In fact, verification is the most time-consuming part of modern system design. Some recent statistics show verification may take up to 60~80% of the total design time and may require a 3-to-1 ratio between verification engineers and circuit designers. Therefore, developing effective verification techniques has great impact on system design. Some topics of interests include sequential equivalence checking, property checking, arithmetic circuit verification, verification for cyber-physical systems, functional timing analysis, web security analysis, and other subjects. We also research on core computer science problems, including satisfiability (SAT) solving, quantified Boolean formula (QBF) solving, dependency QBF solving, and other subjects.

As IC manufacturing process advances, design paradigms shift. Under stringent design criteria, exploiting optimal solutions in various abstraction levels is desperately needed. Some topics of interests include asynchronous circuit synthesis, synthesis from temporal specification, language equation solving for digital circuit optimization, statistical analysis and optimization for VLSI manufacturability, and other subjects.

Tomorrow's important technology breakthroughs stems from today's basic research. It is interesting to explore what we can build from non-conventional computation models and emerging technologies. Some topics of interests include quantum computation, computation with biochemical reactions, neuromorphic computation, and other subjects.