介紹

現在，我很榮幸為大家介紹今年圖靈獎講座的會議主席。這位會議主席是傳奇人物 Amir Pnueli，他曾在1996年獲得圖靈獎。他是位於以色列的 Weissman Institute of Science 以及 New York University 的教授。他因其開創性地將時態邏輯引入計算機科學的工作，以及對程式和系統驗證的傑出貢獻而獲得圖靈獎。我很榮幸 Amir Pnueli 今天能來到這裡主持這場會議。接下來就交給您了。好的。好的，非常感謝您如此精彩的介紹。好的，稍微調整一下。好的，能主持這場會議，對我來說是莫大的榮幸與殊榮，同時也是個人的愉快。正如您所見，這是一份榮譽，因為這是一個重要且盛大的場合，圖靈獎委員會決定表彰和肯定我們三位最傑出的計算機科學家 Ed Clark、Ellen Emerson 和 Joseph Sifakis 多年來在發明和發展自動驗證這一偉大想法方面的成就。這不僅是對他們的肯定，在某種意義上也是對所有關注形式化方法的人的慶祝，因為這肯定了該領域作為一項重要且值得獲獎的事業。這也是個人的愉快，因為這三位獲獎者多年來都是我的私人朋友和同事。我很高興也很開心有這個機會主持這場會議。所以，我將非常簡要地總結一下他們的成就以及獲獎的原因，同時也想補充一些評論，儘管在座的各位對驗證或模型檢測的概念已經非常熟悉，無需介紹。我們都知道，大多數計算機應用都是透過程式在標準硬體或某些情況下的專用硬體上執行的，當然，嵌入式系統和反應系統是特別困難和具有挑戰性的系統類型，我們需要確保它們的正確性。我認為，阻礙我們能夠擁有更廣泛和更深入應用的一點，並非硬體速度慢——硬體當然可以更快，那會非常好——但主要的障礙確實是我們可靠地構建大型、複雜和安全關鍵系統的能力。所以這是仍待解決的挑戰之一。它已經存在一段時間了，並將持續存在一段時間。而這三位獲獎者為解決這個問題做出了非常重要的貢獻。

可靠系統的構建必須進行的核心活動是驗證。在驗證中，我們不深入任何技術細節，總的來說，系統應該滿足某個性質，這通常與其規格或正確性概念相關，而我們想要確定、驗證或建立的是確保系統的所有行為——我特意使用了「行為」這個詞，因為當我們談論嵌入系統和反應系統時，這正是我們運行這些系統以獲得其持續且有趣的行為的主要原因。因此，在目前的實踐中，大多數情況下，大多數地方，在工業應用中，驗證的方法今天仍然主要是動態驗證，這是一種對測試的花哨稱呼。我們在大量輸入和大量情況下運行它，希望如果存在錯誤，我們能足夠長時間且足夠廣泛地對系統進行測試，就能捕捉到大多數錯誤。但這充其量只是一種不完整的方法，我們可以引用 Dijkstra 的話，他是提出這些問題並作為該領域主要創始人之一的貢獻者，他說測試只能發現錯誤的存在，而不是其不存在。而如果您想驗證一個系統，特別是一個安全關鍵系統，獲得完整性、確保沒有錯誤逃脫我們的注意是非常重要的。

與動態驗證或測試不同，形式驗證旨在實現這種完整性，並以數學確定性保證系統滿足其規格或期望的性質。現在，早在67年就已經開始了大量的研究，但最初大部分是理論性的，依賴於定理證明等活動。因此，完整性以及非常高的嚴謹標準得以建立。然而，當時提出的技術非常耗費人力，需要用戶極大的獨創性，並且對許多用戶來說並不廣泛可及。因此，我們今天這三位獲獎者的主要開創性貢獻在於發明了自動形式驗證的方法和想法，我們以某種方式系統地探索系統的所有可能行為。這種方法現在稱為模型檢測，並在2007年，就在差不多一年前，這項開創性貢獻獲得了肯定，這三位科學家因發明模型檢測而獲得了圖靈獎。

從某種意義上說，人們通常將圖靈獎稱為計算機科學的諾貝爾獎，我認為這是一個很好的類比，但還是有一些區別。其中一個重要的區別是，諾貝爾獎通常頒發給一項開創性且非常重要的貢獻，通常不是非常近期的，因為你需要讓時間過去，確保這個想法確實經得起時間的考驗。然而，從某種意義上說，我認為與諾貝爾獎不同，圖靈獎的要求甚至更高，更嚴格。這是一個較年輕的獎項，所以它可以允許自己更嚴格。因此，圖靈獎通常不僅要求您很久以前做出了一項非常重要且開創性的貢獻，而且這項貢獻經受住了時間的考驗，而且，在考慮圖靈獎決定時，獲獎者持續做出重大貢獻也是非常重要且有力的證據。我想用我剩下的兩分鐘時間告訴大家，這三位科學家確實不僅提出了自動驗證的原始想法，而且實際上持續引領著這個領域，並創建了一個新的學科，即主要基於模型檢測的自動或計算機輔助驗證學科。所以我認為，毫不誇張地說，這三位科學家實際上創立並領導了過去27年左右的計算機輔助驗證領域。例如，Ed 和 Joseph 是非常重要且活躍的年度計算機輔助驗證會議 CAV 的兩位創始人之一，多年來，自動驗證領域的大多數新想法都是在那個會議上探索的。

此外，我還可以講一些關於每位獲獎者個人貢獻的事實。我必須向他們道歉，這是一個非常簡略、非常電報式的提及一些成就。這當然不應該是全面的，只是指出這三位獲獎者貢獻的重點。所以，讓我按字母順序從 Ed 開始。當然，Ed 在模型檢測和自動驗證引入的幾乎所有重要趨勢和新想法中都起到了非常關鍵和引領作用。舉一些例子，他參與並高度促成了——他也因此獲得了共享獎項——符號模型檢測的引入，這使得我們能夠擴展規模並考慮非常大的系統，當然這與他的學生 McMillan 以及 Ellen 和 Bryant 共同完成。此外，他是第一個說，這不是進行模型檢測的唯一方法，我們應該開始關注 SAT，這目前是處理比以前可能處理的更大的系統的競爭方法之一。他在推動，或廣泛推動從硬體模型檢測（這是一個巨大的成功故事，這本身就是一個故事）轉向自動驗證目前面臨的挑戰，即軟體模型檢測方面非常有影響力。為了實現這一點，他非常努力地推動抽象和抽象精化的想法，引入了現在廣泛用於軟體驗證的方法論，稱為 CIGAR 方法論，其中您使用反例作為反例來改進您的抽象。當然，抽象是使用模型檢測（本質上適用於有限狀態系統的技術）來處理軟體驗證（本質上是驗證無限狀態系統）的唯一方法。

接下來是 Ellen Emerson，Ellen Emerson 在理論方面做出了非常強大、非常重要的貢獻。他負責引入了表達能力最強的時態邏輯 CTL*，並提出了一些方法來驗證這種複雜的邏輯。他還教導我們很多關於如何使用 mu 演算作為規格語言以及一種非常強大的驗證技術。這現在在驗證中無處不在，也在新興的程式合成或系統合成領域中使用，mu 演算是人們用來解決博弈和類似問題的主要工具。

最後，Joseph Sifakis 研究了許多幫助我們處理更大系統以及更現實模型的主題，因為模型檢測最初設計所基於的模型（稱為模型）是實時並非非常明確的模型。我們無法測量時間，而 Joseph 與其他一些研究人員一起，在實時系統的模型及其驗證方面給予了我們很大的幫助，並且他在混合系統方面非常有幫助和引領作用。最近，他開始研究構建正確系統的替代方法，即「建構即正確」（correct by construction）以及基於元件的程式開發。他現在是 Artist Network of Excellence 的領導者，該網絡專注於嵌入系統和構建正確系統的新方法。

我不佔用您更多時間了。總之，這三位獲獎者對該領域的現狀做出了非常重要且開創性的貢獻，實際上塑造和引領了該領域達27年，從那以後，他們一直持續引領並做出傑出的貢獻。

圖靈獎，祝願他們未來多年研究成果豐碩，貢獻卓越。好的，非常感謝。我想接下來我們要看看一段短片，回顧一下圖靈獎頒獎典禮本身的情況。所以，請播放影片。

圖靈獎的歷史與意義

1938年，Alan Matheson Turing 憑藉其關於可計算數的經典論文開啟了現代計算機時代。從那時起，他的思想對計算的發展產生了巨大影響，這種影響持續至今。在獲得 Princeton University 數學博士學位後，他回到英國，成為 King's College 的研究員。二戰爆發後，他在英國政府的政府密碼學院任職，在那裡他在破解德國 Enigma 密碼方面發揮了關鍵作用，這對贏得盟軍勝利至關重要。1945年，他領導團隊設計並建造了 Automatic Computing Engine，或 ACE，這是一台重要的早期電子數字計算機。他的幾篇論文現在被廣泛認為是人工智能研究的基礎。他提出了稱為圖靈測試的標準，這是他提議用於判斷機器是否真正能夠思考的方法。如今，這仍然是衡量人工智能的標準。1966年， Association for Computing Machinery (ACM) 設立了圖靈獎，以紀念 Alan Turing。多年來，它已成為全球公認計算領域最負盛名的獎項，每年頒發給對計算社區做出持久重大技術貢獻的個人。我們所有人都對 Alan Turing 負有巨大債務。正是他的獨創性和遠見幫助實現了計算機革命。ACM AM Turing Award 的財務支持由 Intel Corporation 和 Google 提供。好的。

我很榮幸介紹第一位發言人，再次按字母順序。Ed Clark，請。

謝謝大家。首先，我要感謝 ACM 頒發這份令人難以置信的獎項。自去年二月宣佈以來，這確實是令人驚奇的一年。我也要感謝 ESWeek 和 MSOF 主辦我們的演講。我想不出還有哪個會議比這裡更適合我們介紹這些材料。我還要感謝 Amir Pnueli 熱情的介紹。當然，如果沒有他1977年的開創性論文，我們今天就不會在這裡談論模型檢測時態邏輯規格。

模型檢測簡介

模型檢測是一種自動驗證技術。它已成功用於驗證通信協議和硬體設計，並且也開始用於軟體驗證。模型檢測的主要缺點是狀態爆炸現象，我猜想你們中許多人都很清楚並因此受苦。在過去的27年裡，這一直是我的探索，而且這確實是一場探索，以開發克服這個問題的新方法。正如您將看到的，我們在這個問題上確實取得了一些進展，但它將永遠伴隨著我們，我們必須繼續尋找新的、更好的方法來擴大模型檢測的力量。

現在，為了讓您對模型檢測能做什麼有一些概念，我想從一個例子開始。這是一個老例子，但有些人可能還記得。它是1994年第一代 Pentium（Pentium I）的浮點除法錯誤。Intel 在 Pentium 中使用 SRT 除法算法進行浮點除法，並且表格中缺少了五個條目，導致了這個錯誤。硬體錯誤尤其令人頭痛，因為通常您不能簡單地發送軟體補丁，您實際上必須更換晶片。估計為了解決這個問題，Intel 花費了4億到5億美元。

Intel 宣佈 Pentium I 晶片確實存在問題後不久，我的一位前 CMU 學生 Manpreet Kaira，當時正在 Intel 工作，打電話給我說，請派一位您的學生過來。我派去了 Zudong Zhao，他是當時我最好的學生。Zudong 在 Intel 工作了三、四個月，並證明了他的論文主題——字級模型檢測——確實可以找到 Pentium 的錯誤。而且，他還證明了 Intel 提出的修復方法確實解決了問題。

不幸的是，或許對於我們這些從事驗證行業的人來說是幸運的，硬體錯誤仍在不斷發生。就在去年，AMD 處理器似乎在翻譯後備緩衝區（translation look-aside buffer）出現了問題。據我所知，這實際上延遲了處理器的發佈日期。AMD 沒有正式宣佈此事，所以我在這裡打了兩個問號，表示這確實是一個傳言。但如果你用 Google 搜尋「AMD Barcelona bug」，那些帶著筆記本電腦的人，你會發現很多關於這個特定問題的討論。

模型檢測是一種自動驗證技術。它最初是為推理有限狀態並行系統而開發的。它是由 Alan Emerson 和我以及當時在 University of Grenoble 的 Queille 和 Sifakis 獨立開發的。我認為這確實是對一個重要概念的獨立發現。我們的論文發表在 Springer Lecture Notes 131 中，我想他們的論文發表在 Springer Lecture Notes 137 中，差不多是這樣。所以他們絕對應該獲得同等的貢獻。這些技術也非常相似。

模型檢測中的規格是用命題時態邏輯編寫的。命題時態邏輯，正如你們大多數人所知，是一種用於推理事件在時間上的順序，而不明確引入時間的表示法。它由 Amir Pnueli 在他1977年的論文中首次用於指定並行程式。驗證過程是... 基本思想其實非常簡單。它是一種智能的、窮盡性的狀態空間搜索，以確定公式是否成立。但多年來，我們必須玩一些技巧來擴展這種技術。

模型檢測的優勢

模型檢測相對於其他驗證方法有許多優勢。首先，您不必構建證明。模型檢測是算法性的，不是演繹性的。當它適用時，它通常比其他嚴謹的技術（例如交互式定理證明，可能需要數月與證明檢查器一起工作來證明一個相對簡單的程式是正確的）要快。如果規格不滿足，模型檢查器會產生一個診斷性的反例，顯示規格為何不正確。部分規格沒有問題，您無需完全指定系統就可以開始獲得關於其正確性的有用信息。並且邏輯可以表達許多您需要用於推理並行系統的性質。

我認為，最重要的特性可能是反例特性。低估這個特性的重要性是不可能的。有些人使用模型檢查器只是為了獲得設計中隱藏錯誤的好的反例。一個反例軌跡可以直接帶您找到一些非常隱藏的錯誤的源頭。

狀態爆炸問題

狀態爆炸問題很容易理解。一個兩位計數器有四個狀態。當然，我們都知道一個 n 位計數器有 2 的 n 次方個狀態。狀態爆炸問題也可能因處理或離開而發生。如果我們有兩個並行進程，那麼它們的異步組合將有九個狀態。一般而言，如果我們有 m 個進程，每個進程有 n 個狀態，那麼它們的並行組合將有 n 的 m 次方個狀態。

可以透過簡單的複雜性理論論證證明，在最壞情況下，狀態爆炸問題是不可避免的。在最壞情況下，你真的無能為力。但我們多年來一直保持樂觀，並通過使用巧妙的算法、複雜的數據結構和良好的工程，在這個問題上取得了穩步的進展。

時態邏輯的類型

現在，有兩種時態邏輯。線性時態邏輯（Linear Temporal Logic），它在無限軌跡上確定路徑。公式由原子命題、布爾運算和時態算子構成。命題 A 對於一個軌跡成立，如果 A 標記了該軌跡的第一個狀態。X A 對於一個軌跡成立，如果 A 在該軌跡的下一個狀態成立。F A

g 必然會變為真。ag g 對於這棵計算樹的根部會成立，因為沿著每條路徑 g 都全局成立。我們會說 g 是一個不變式，或者說 g 在每個可到達的狀態都成立。eg g 對於這棵計算樹的根部會成立，因為存在一條路徑，並且 g 在該路徑上全局成立。g 有可能永遠成立，g 是一個潛在的不變式。

現在，CTL 使用了我剛才描述的四個算子，加上 next time 算子的全稱和存在版本，以及 until 算子的全稱和存在版本。CTL* 是一個表達能力更強的邏輯，它允許更豐富的時態算子嵌套類型，可以表達分支時間和線性時間性質。

模型檢測問題

模型檢測問題的表述和理解都很簡單。如果我們有一個狀態轉移圖和一個時態邏輯規格，那麼模型檢測問題就是找到結構 m 中所有使公式為真的狀態 s。雙橫線符號表示在結構 m 的狀態 s 處為真。

模型檢測算法早在80年代就已經提出，適用於 CTL、LTL、CTL*。基於自動機理論的模型檢測算法也已經提出，至今仍經常用於 LTL。其中一種算法由我自己、Alan Emerson 和 Prasad Sisla 開發，其複雜性與模型的大小和公式的大小呈線性關係，即與它們的乘積呈線性關係。儘管該算法具有線性複雜性，但在實踐中其用處有限，因為存在狀態爆炸問題。模型常常大到無法放入計算機的內存中。

現在，為了讓您了解模型檢測如何使用，假設您開發了一個新的微波爐。我確信你們大多數人比我更了解模型檢測的用途，但我將在這場演講中假設您沒有任何關於模型檢測的先驗知識。假設對於微波爐，我們有這個控制器，這個微波爐的有限狀態控制器。那麼我們希望微波爐滿足的一個性質是，在門關閉之前它不會加熱。我們不希望任何人被燙傷。好的，我們可以將其更簡潔地表達為「不加熱直到門關閉」。這可以直接映射到時態邏輯中，表示為 not heat up until door closed。波浪號表示 not，U 是 until 算子。現在，模型檢查器會接收這個公式，並檢查它是否在我在前幾張幻燈片中展示的狀態轉移圖中的所有路徑上成立。如果它成立，它會告訴我們公式為真。如果它不成立，它會給我們一個反例。

模型檢測流程

在模型檢測中，我們通常從規格開始。如果是硬體驗證，我們會從 Verilog、VHDL 或 SMV 的規格開始，以及自然語言（如英語）的非形式化規格。我們會將硬體描述編譯成一個狀態轉移圖，我們會將非形式化規格轉換（通常是手動）成一組時態邏輯公式。模型檢查器將算法性地確定時態邏輯公式對於轉移系統是否為真。關鍵部分是使這種算法檢查盡可能高效。

狀態爆炸問題的四大突破

在我看來，關於狀態爆炸問題有四大突破。

第一個是帶有有序二元決策圖 (OBDD) 的符號模型檢測。第一個模型檢測算法使用狀態轉移圖的顯式表示，即鏈接列表結構，這是所有算法文本告訴你表示圖的方法。Ken McMillan 在1987年來到 CMU 的前六週內，提出了一種更好的表示狀態轉移圖和狀態集的方法。他認為這種顯式表示非常浪費，如果我們使用二元決策圖顯式表示狀態轉移圖，那麼我們可以檢查更大的系統。我們實現了他的算法。他在論文中開發了 SMV 模型檢查器。它至今仍被廣泛使用，可以從 Cadence 或新的 SMV 網站下載。我們能夠檢查一些最初有 10 的 20 次方個可到達狀態的例子，然後我們甚至能夠檢查一些有 10 的 120 次方個可到達狀態的例子。這顯然是一個重大的突破。符號模型檢測至今仍被廣泛使用。

另一個突破是我沒有參與其中，但我認為它異常重要，那就是偏序約減。在異步系統中，有時會有可交換的動作。例如，如果我們先做 A 再做 B，我們得到與先做 B 再做 A 相同的結果。當這種情況發生時，您可以利用這些知識來減少必須考慮的交錯數量。我認為第一個提出偏序約減想法的是 Antti Valmari，隨後是 Patrice Gribomont 和 Doron Peled。Doron 使用 Ample sets 的實現是在 SPIN 模型檢查器中使用的實現，這也是其大部分力量的來源。

下一個重大突破是使用快速 SAT 求解器的有界模型檢測。現在，如果我在1976年讀研究生時說我要為我的博士論文研究 SAT 求解，那麼人們會嘲笑我，我也可能永遠無法獲得學位。我的意思是，CNF SAT 是規範的 NP-complete 問題，是第一個 NP-complete 問題。然而，現在看來，許多在實踐中出現的 CNF 公式即使它們體積巨大，也可以檢查其可滿足性。一些具有數百萬個文字、數百萬個變量和數千萬個子句的公式可以在幾分鐘內檢查其可滿足性。現在可以處理數千個鎖存器，而不是像使用 OBDD 那樣只能處理數百個鎖存器。

這裡有一個關於有界模型檢測如何工作的小例子。假設您想知道某個性質 P 是否會在 K 個步驟內失敗。我們以布爾變量向量的形式符號化地表示系統的狀態，我們假設我們有一個謂詞 I(P)，如果一個狀態是初始狀態，則該謂詞為真；T 是系統的轉移關係；P 是該性質。所以這個公式對於一個路徑 V0, V1, V2 到 VK 會為真，如果該路徑始於一個初始狀態：I(V0) 且從 V0 到 V1 有一個轉移，從 V1 到 V2 有一個轉移，以及從 VK-1 到 VK 有一個轉移。並且規格 P 在這些步驟中的某一步為假。現在，我們將這個公式提交給一個 SAT 求解器，順帶一提，這推廣到所有的 LTL，我們將這個公式提交給一個 SAT 求解器，SAT 求解器將為這些變量尋找一個滿足實例，為狀態變量向量 V0, V1 到 VK 尋找滿足實例。如果找到了，它就可以立即從該賦值中讀取一個反例。現在，如果找不到怎麼辦？這裡有一點問題。我們不知道是否根本沒有反例，並且電路是正確的，不管您展開多少步，P 都不可能失敗。或者可能只是這樣，如果我們再展開一次轉移關係，展開 K+1 步，我們就會找到一個稍微長一點的反例。所以，仍然需要做一些工作來使有界模型檢測完整。有一些技術可以確定您需要展開轉移關係多遠，才能確保如果存在反例，您就可以通過展開到該深度找到它。

現在，這裡有一個 Armin Biere 最近發給我的例子。這是一個有10,000個鎖存器、10,000個輸入的電路的例子。Armin 檢查的問題的公式有400萬個變量，1200萬個子句，而最短的長度為37的錯誤在69秒內被找到。我認為這非常了不起。自從我們在第一代模型檢查器上檢查10個狀態機以來，我們已經取得了長足的進步。

因此，第四個重大突破是局部化約減或反例引導的抽象精化 (CGAR)。1994年，Bob Kurshan 寫了一本關於基於自動機理論驗證的書。書中有一個我一直無法理解的部分，那就是他關於局部化約減的部分。Bob 一直告訴我這很重要，但我似乎就是跟不上所有的細節。然而，我的一位學生 Yuan Liu 沉迷於理解它，並找出它為何如此出色。他成功了。他設法弄明白了局部化約減為何重要。我們發現它根本沒有那麼難理解。我們以一種方式將其推廣，使其可以用於軟體模型檢查器。原始版本是為處理電路中的鎖存器而編寫或開發的。所以我們必須做一些工作，使其適用於程式。它在大多數（但不是所有）軟體模型檢查器中使用。

現在，CGAR 如何工作。我們從一個程式或電路開始。我們形成程式或電路的保守過度逼近（conservative over-approximation），使得這個抽象模型具有程式或電路的所有行為。然後我們對抽象模型進行模型檢測，這個模型據說比原始程式或電路具有少得多的狀態。這可以直接使用現成的模型檢查器，如 SMV 或 SPIN。如果我們沒有得到錯誤，那麼我們就知道性質在原始程式上成立，因為我們處理的是原始程式的過度逼近。如果我們確實得到錯誤，如果我們找到一個反例，那麼我們必須檢查並確保這不是抽象過程引入的軌跡。所以我們必須在具體模型，即原始模型上模擬它。

因此，我們利用該反例中的信息來精化抽象，並循環回去。該技術在幾種軟體模型檢查器中都有實現。我稍後會特別提到其中一種。

軟體與嵌入式系統的驗證挑戰

一個自然的問題是，是否有可能從硬體轉向軟體？在 Wired News 2005年11月10日的報導中，Bill Gates 宣佈他們正在開發一種軟體分析工具，可以找到 Windows 設備驅動程式中的錯誤。他稱之為計算機科學的「聖杯」。

是什麼讓軟體模型檢測與硬體模型檢測不同？原因很多。整數、浮點數、字符串、用戶定義類型和類、帶別名的指針、堆中分配的無限數量單元、過程調用、遞歸、通過指針調用、動態方法查找、重載、具有無限數量線程的並發、模板、泛型、包含文件、中斷、異常、回調、使用輔助存儲文件、數據庫、庫的源代碼缺失、系統調用、移動代碼、不常見的特性，如延續（continuations）和自修改代碼。最後但同樣重要的是，純粹的長度。Microsoft Word 的代碼行數遠超一百萬行。

軟體模型檢測已經取得了一些成功。我認為最成功的軟體模型檢查器是 Microsoft 開發的 Static Device Verifier (SDV)。我之前引用的同一個 Wired News 報導中提到，Microsoft 開發了一個名為 Static Device Driver 的工具，它使用模型檢測來分析 Windows 設備驅動程式的源代碼，並檢查程式員編寫的代碼是否與 Windows 設備驅動程式應該做什麼的數學模型匹配。如果不匹配，則 SDV 會警告驅動程式可能包含錯誤。順帶一提，Microsoft 聲稱 Windows 經常崩潰的原因是第三方設備驅動程式。我自己對此有些懷疑。

未來的挑戰

這把我帶到了演講的結尾，或者幾乎到結尾：未來的挑戰。有很多。模型檢測還很年輕。我認為在利用 SAT 的力量方面還有很多工作要做。每年都有 SAT 競賽，每年 SAT 求解器都變得更快。它們的速度每年仍然翻倍。此外，快速 SAT 求解器使得一些經典的判定過程變得可行，例如無量詞的 Presburger 算術。您可以在實踐中實際使用它們。這方面有很多研究。

軟體和硬體的組合模型檢測。如果有一個系統，將其分解為部分，分別驗證這些部分，然後對整個模型做出結論，通常是有利的。現在，我們剛開始意識到，我們認為對組合模型檢測有效的技術並不那麼有效。它的擴展性不如我們預期。所以，在使組合模型檢測有效方面還有更多工作要做。

軟體模型檢測是一個巨大的挑戰性問題。我不認為在不久的將來它會變得常規。然而，現在可以將模型檢測與靜態分析技術結合起來，並在軟體中找到錯誤。但要說使用模型檢測技術證明一段軟體實際上是正確的，還有很多工作要做。

嵌入式系統的驗證。這實際上本身就是一個主題，對於本次會議來說是一個非常非常重要的主題。目前最好的混合自動機模型檢查器（針對同時具有離散和由微分方程控制的連續演化的系統）只能處理少數幾個變量。這令人失望。我們真的需要做一些事情。這個領域迫切需要突破。模型似乎不錯，但目前開發的技術擴展性不好。所以，這方面需要大量研究。

模型檢測和定理證明。我不是模型檢測的頑固分子。我相信將模型檢測與其他技術結合起來很重要，不僅是靜態分析，還有定理證明。一些定理證明系統中的模型檢查器，例如 MAUDE 中的，非常強大，並且已經取得了令人印象深刻的結果。

概率模型檢測和統計模型檢測，我認為很重要。我目前正在研究統計模型檢測。我相信這項技術可以用於連接隨機測試和模型檢測。您可以通過生成大量軌跡並在這些軌跡上檢查公式來得出結論。您實際上可以給出規格不成立的概率上限。

隨著模型的規模變得如此之大，反例也隨之增長。光是弄清楚反例出了什麼問題或反例說明了什麼就是一個大問題。

最後，擴大規模。我們將永遠面臨這個問題。我們將始終需要提出更好的模型檢測技術。

我自己的目標是研究安全關鍵嵌入式系統的驗證。你們大多數人可能知道，或者我確信你們都知道，汽車正朝著線控驅動發展。我認為如果發生這種情況，我們將不得不驗證汽車內部的電路。Amir，我快說完了。再過一頁幻燈片。我正在與 GM India Science Lab 的一些人合作進行這個項目。

在這場探索中，在我27年的探索中，我獲得了許多幫助。所以我想要展示這張幻燈片。這是我過去27年來的博士生、博士後和訪問學者列表。與他們一起工作真的很愉快。而真正應當歸功於我的突破的人是他們。