Formal verification is a technique which analyzes system behaviors and hence improves system quality. For the past three decades, formal verification has significant impacts on both academics and industry. From hardware circuits and network protocols, to device drivers, operating systems, and compilers, formal verification is essential to the design of high-quality systems. 

For the past years, I have been working on various formal verification techniques in different computation models. The SAT-based local model checking generalizes inductive proofs to verify branching time properties on hardware circuits. Several learning-based assume-guarantee reasoning techniques are also developed for concurrent classical and probabilistic systems. Algorithmic learningis also applied to infer loop invariants and termination proofs on imperative programs. My researches aim to advance practical formal verification by applying theoretical ideas.

In the near future, I plan to explore new applications for formal verification. In data parallel computing, developers write programs in new parallel programming models. Unlike models for general parallel computation, such programming models are optimized for data analysis and have fixed communication patterns. New programming errors are also introduced by new models. In the past, research communities mostly focus on exciting applications of data parallel computation. Correctness of parallel data analysis programs is often overlooked. My recent work tries to bring attention to the formal verification community. 

Another application of interest is privacy issues in data analysis. Privacy is undoubtedly a hot topic in the age of big data. Research communities have also tried to develop privacy-respecting mechanisms in both theory and practice. Yet an ill-implemented mechanism can lead to privacy intrusion. One has to analyze implementations to attain one''s privacy. This clearly opens the door for formal verification. In order to apply formal verification, privacy has to be formalized. New verification techniques are also needed. Hopefully, my current research will give some insights to the problem in the near future.