Current and Past Funded Research:
Design and Verification of Hardware/Software Systems

• Scalable Co-Verification Based on Hardware IPs and Software Component, SRC
  The objective of the project is to develop a component-based approach to scalable hardware and software co-verification of embedded systems using model checking, which unifies the concepts of hardware IPs and software components, leverages advances in assertion-based verification, extends effectiveness of compositional model checking for system-level co-verification, and facilitates verification reuse.
• Formal Verification by Generalized Symbolic Trajectory Evaluation, Intel
  Generalized symbolic trajectory evaluation (GSTE) is an extension of symbolic trajectory evaluation (STE). STE can handle large, industrial design and has been actively used in Intel, HP, IBM, and Motorola. GSTE was originally developed at Intel and has successfully demonstrated its powerful capacity in formal verification of digital systems. The goal of the project is to enhance the GSTE verification capability for complex system designs.

Back to Research Activities