模型檢驗和自動定理證明是正規驗證中，兩種最具潛力的技術。在模型檢驗中，電腦系統的數學模型針對其正規規格進行檢查。這個以模型理論為基礎的技術能有效率地探索有限狀態模型，並已被廣泛地應用於電腦硬體系統的設計。另一方面，電腦系統則在自動定理證明技術中被正規化為邏輯理論。系統之驗證則等同自這些邏輯理論推導數學定理。這個以證明理論為基礎的技術能正規地檢查數學證明。而由於自動定理證強大的表現能力，它被廣泛地運用於如電腦軟體系統等無限狀態系統之驗證。上述兩種技術各有其優劣，沒有任何一種得以令人滿意地驗證任意的電腦系統。因此，如何結合此兩種技術，以發展混合的新技巧，則是一項相當有趣的研究問題。

        我的研究興趣包含了在正規驗證中模型檢驗和自動定理證明兩項技術。在模型檢驗方面，我們基於證明理論架構上，發展了一個完備的模型檢驗演算法。在此架構上，模型檢驗演算法成了證明搜尋。而我們的模型檢驗演算法則利用先進的SAT引擎以搜尋證明，也解決了模型檢驗問題。這個證明理論為基礎的方法，事實上比傳統以利用SAT引擎的模型檢驗演算法更為廣泛。首先，新的方法能驗證比傳統方法還更具表現能力的邏輯。其次，它已被應用於驗證context-free processes。我們的方法不只能檢驗更多的性質，還能檢驗無限狀態的系統。傳統利用SAT引擎的技術，尚未能達同時被推廣於此二方面。

        組合式分析是減低狀態爆炸問題中，最有效的方法之一。在組合式分析中，系統之驗證依證明規則而分解成若干關於組成份子之驗證工作。藉由組合證明規則之正確性，系統之正確性可由其組成份子之正確性而得之。由於各組成份子可各自被驗證，狀態爆炸問題因此而被避免。但是發展正確的組合證明規則，卻依賴於性質和計算模型。事實上，過去數十年來，許多的研究已投入此項工作。針對有限狀態自動機和軌跡語意，我們發展了一套自動化的技術，得以推導組合證明規則。除此以外，我們還證明了prefix-closed 規則語言形成Heyting 代數。因此，直觀邏輯的證明系統LJ 可以推導在此類規則語言所適用之組合證明規則。

        在應用自動定理證明的第一步驟，是在所使用之證明程式中正規化問題。於正規驗證中，吾人必須將不同的時態邏輯和計算模型建入，並實行正規定理證明。事實上，linear temporal logic 和computation tree logic 已被建於各種不同的定理證明程式中。不過，一旦時態邏輯或計算模型在各別應用中改變，這個正規化工作則必須重新於執行。我們為CTL* 進行模組式的正規化，以解決此一問題。CTL*比linear temporal logic 和computation tree logic 還要具表現性。除此之外，這個模組式的正規化於Coq 的模組系統中，明確地說明計算假設。若要重覆使用這個正規化，使用者只須正規地建立這些假設。利用我們模組式的正規化，我們已經證明大部份的LTL，UB，CTL 和CTL*正確性定理。而由於模組化，這些證明在未來的應用中，無須被重新建立即可被使用。