- Automated compositional verification
- Automata-based model checking
- Verification of programs on multicore computers
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.