美國卡內基梅隆大學計算機系教授、中國科學院「愛因斯坦講席教授」、圖靈獎得主EdmundClarke於10月20日至27日對蘇州研究院進行了為期8天的學術訪問與交流。
Edmund Clarke教授是形式化驗證領域中模型檢查(Model Checking)技術的創始人之一,美國計算機學會(ACM)與美國電氣電子工程師學會(IEEE)院士,同時也是美國國家科學院和工程院院士。Clarke教授於2007年和另外兩位科學家E.Allen Emerson和Joseph Sifakis一同分享了「圖靈獎」,以表彰他們對模型檢查理論與技術做出的奠基性貢獻。目前模型檢查技術已成為一個被廣泛應用在硬體和軟體工業中非常有效的驗證技術。
10月21日上午,Clarke教授為蘇州研究院的師生帶來了題為「Model Checking and the Curse of Dimensionality」 的精彩報告。Clarke教授在演講中回顧了模型檢查理論技術的發展歷程,分析了在過去20多年裡面遇到的四個典型的難題,講解了科研人員如何解決這些難題並取得重大突破。
10月22日上午,Clarke教授針為中科大-耶魯高可信軟體聯合研究中心師生作題為「Symbolic Model Checking with BDDs」的講座,深入淺出地介紹了符號化模型檢查的由來與基本算法原理,還興致勃勃地講述了在1992年他與他的學生們採用該模型檢查算法檢測到一個緩存一致性協議存在缺陷的故事,這一協議來自一個當時已經公布四年之久的工業標準協議(IEEE FutureBus+ Standard)。這是第一個採用形式化方法在IEEE標準中找到錯誤的應用案例,展現了模型檢查方法在工業硬體設計領域中的應用前景。
10月23日上午,Clarke教授為研究中心師生帶來了第二場專場講座,題目為「Bounded Model Checking with SAT/SMT」。Clarke教授在這個講座中重點講述了他在模型檢查方法中取得的一個重大突破——目前已在工業界廣泛採用的基於SAT工具的限界模型檢查方法。研究中心的師生表示通過這個內容詳實的講座學習到了模型檢查最前沿的研究成果與工業應用,收穫頗豐。
隨後的幾天裡,Clarke教授與研究院的師生進行了面對面的深入交流,並聽取了中科大-耶魯高可信軟體聯合研究中心、嵌入式系統實驗室等團隊的工作介紹。Clarke教授對蘇州研究院各團隊的研究課題表示出了極大的興趣,並提出了寶貴意見。
(計算機學院、蘇州研究院)