15日上午，“愛因斯坦講席教授”證書授予儀式暨報告會在軟件所5號樓315會議室舉行。會上，軟件所所長李明樹代表中國科學院為Edmund M. Clarke教授頒發了“愛因斯坦講席教授”證書。 

儀式結束后，Clarke教授作了題為Model Checking and the Curse of Dimensionality的學術報告。報告中，Clarke教授淺入深出地對模型檢測技術進行了闡述。模型檢測是一種自動驗證技術，由Clarke、Emerson和Quielle、Sifakis分別在1981年獨立提出，在過去三十年中對計算機科學的理論和實踐都產生了重大的影響，取得了極大的成功，并在工業界得到了廣泛的應用。

在講到模型檢測技術面臨的挑戰時，Clark教授介紹了近三十年來在解決狀態空間爆炸問題方面所取得的幾個里程碑式的進展。他還介紹了模型檢測技術在軟件、信息物理融合系統、生物信息學等領域的應用前景。 

16日上午，在題為Symbolic Model Checking with Ordered Binary Decision Diagrams的報告中，Clarke教授介紹了其在符號模型檢測方面的研究。他認為，符號模型檢測技術是自動驗證領域的重要貢獻之一，而有序二叉判定圖（OBDD）的唯一性是符號模型檢測技術成功的關鍵。 

17日上午，Clarke教授作了題為Bounded Model Checking with SAT/SMT的報告。報告主要講述了其在限界模型檢測方面的研究，并介紹了其團隊在復雜混成系統驗證方面的最新研究成果。報告中，Clarke教授還鼓勵探索不同分析、驗證技術（如定理證明、靜態分析等）的有機結合。 

三場報告內容精彩，激起了大家的濃厚興趣。Clarke教授回答了大家提出的大量問題，并就組合驗證、概率模型檢測等學術問題進行了熱烈的討論。 

15日下午和18日上午，Clarke教授還聽取了實驗室研究人員在符號模型檢測、限界模型檢測、混成系統驗證、概率模型檢測及假設—保證推理等方面的工作報告，并就相關技術細節進行了深入、細致地討論，雙方對促進未來合作研究都充滿期待。 

Clarke教授1967年在弗吉尼亞大學獲得數學學士學位，1968年在杜克大學獲得數學碩士學位，1976年在康奈爾大學獲得計算機博士學位。然后，Clarke教授在杜克大學任教兩年，于1978年加入哈佛大學并擔任助理教授。1982年，加入卡內基梅隆大學計算機系。Clarke教授曾獲IEEE Harry M. Goode紀念獎（2004年）， ACM圖靈獎（2007年），Herbrand獎（2008年）。Clarke教授2005年當選美國工程院院士，2011年當選美國藝術和科學院院士。 

講座報告下載地址：http://lcs.ios.ac.cn/feed/?p=877

頒發證書

講座現場

Edmund M. Clarke教授作報告