形式化驗證是一種分析系統行為，藉以增進系統品質之技術。過去三十年來，形式化驗證已在學界和業界有顯著之影響。從硬體電路和網路協定，到驅動程式、作業系統、編譯器，形式化驗證在設計高品質系統為一基本要素。

在過去幾年，我在不同的計算模型上研究各類形式化驗證之技術。以SAT為基礎的局部模型檢測，將硬體電路上之歸納證明推廣至驗證分支時序的性質。也為了古典與機率之並行系統，發展了幾個學習為基礎的組合式分析技術。演算式學習亦被應用於基本程式上，以推導廻圈不變式及中止性證明。我的研究目標在應用理論想法，以增進形式化驗證。

在未來，我計劃為形式化驗證探索新的應用。在平行資料計算中，開發者在新的平行程式模型上寫程式。不同於一般的平行計算，這些程式模型為了資料分析進行最佳化，而有固定的通訊模式。新的程式錯誤也同時被引進這些新的模型中。在過去，研究界大部份注重在平行資料計算上之新奇的應用。資料分析程式之正確性則多半被忽略。我最近的研究成果希望能引起形式化驗證界的注意。

另外一個有趣的應用是資料分析之隱私問題。在大數據的時代，隱私權無疑是一項熱門的課題。研究界也試著在理論及實務上，發展尊重隱私的機制。但是一個不正確的實作，能導致隱私的侵犯。我們必須分析具體的實作以確保個人之隱私。這無疑為形式化驗證開了扇大門。為了應用形式化驗證，隱私必須被形式化。同時也需要新的驗證技術。我希望我的研究，在不久的未來能為這個問題提出一些新的看法。