My main research interest is on automatic techniques (model checking) for verifying correctness of software/hardware system. The main focus is on three topics: The goal of automated compositional verification is to improve the scalability of model checking. In the approach, one applies a compositional inference rule to break the task of verifying a system down to the subtasks of verifying its components. The compositional inference rule is usually in the so-called assume-guarantee style. We proposed several approaches to improve automated compositional verification, which include extending it to allow the verification of liveness property and a new algorithm that guarantees finding the minimal contextual assumption of an assume-guarantee rule.

In contrast to LTL model checking that uses a logic formula to describe the desired property, automata-based model checking allows the use of finite-state machines to describe the property to be verified. This is an on-going research area; many problems remain there to be solved. Scalability is still the main concern. In the previous year, we developed efficient algorithm for minimizing and checking language inclusion of different types of automata, which can be used to improve automate-based model checking.

Recently, I started to investigate programs verification problems on multicore architectures. In recent years, multicore architecture becomes the mainstream of the design of CPUs. Under such architecture, the correctness of a program depends on the memory model it assumes. Besides, programmers usually have to use multithreads for achieving a better performance. Comparing to sequential programs, multithreaded concurrent programs are more prone to error. Therefore, there is an urgent demand for automatic verification. Under multicore architecture, the correctness properties concerned include absence of race-condition, deadlock, livelock, linearizability, etc. The verification of these properties will be more difficult under a weak memory model. I plan to conduct research surround these topics.