Model checking has been successfully used for hardware and software verification. Previous methods were however based on finite-state model checking or pushdown model checking, where systems must be abstracted as finite state systems or pushdown systems before they are model-checked. We are studying higher-order model-checking, where models are described by higher-order recursion schemes. The higher-order model checking subsumes finite-state and pushdown model checking, and is more suitable for verification of higher-order functional programs. In fact, it provides a sound and complete method for various verification problems (e.g. reachability, flow analysis, and resource usage verification) for the simply-typed lambda-calculus with recursion and finite base types. We have implemented model checkers TRecS and HorSat2, and prototype verification tools, MoCHi and EHMTT verifier, on top of it. See our recent papers in JACM (which subsumes POPL 2009 and PPDP 2009 papers), POPL 2010, LICS 2009, and PLDI 2011 for more details.
Following Gordon and Jeffrey's work on type systems for authenticity of security protocols, we have developed an automated type-based verification method for authenticity of security protocols. We have implemented SpiCA2, a type-based, fully-automated verification tool for authenticity in security protocols. See our papers in ESOP 2009 and ATVA 2011 fore more details.
Type systems play an important role in guaranteeing partial correctness of programs. By enriching standard types with various information about program behavior, we can analyze a variety of properties of programs. Our recent work include:
Concurrent programs are hard to read, write, or debug. We have been studying type systems for statically checking behavior of concurrent programs. In particular, we have developed type systems for finding which communication or synchronization is guaranteed to succeed. Based on that work, we have implemented a type-based program analysis tool TyPiCal.
Resources such as files, memory, and network usually are associated with certain protocols. For example, a file should be eventually closed, and it should not be accessed afterwards. A lock that has been acquired lock should be eventually released. We are studying type-based methods for statically verifying that a program conforms to such resource usage policies. See our TOPLAS paper.
Recent studies include type-based transformation of XML tree processing programs into XML stream processing programs (see our papers in APLAS 2004 and LOPSTR 2005), and type-based methods for useless-code elimination (see see our papers in Higher-Order and Symbolic Computation and APLAS2003).
I have been collaborating with Reynald Affeldt to develop a Coq library for verification of conurrent programs.