清華學子面對面對話學術(shù)大師之
圖靈獲得者愛德蒙·克拉克做客“巔峰對話”
清華新聞網(wǎng)4月28日電（研通社記者 方 文 彭智軒 杜林霏） 4月25日下午，清華大學“巔峰對話”活動第二場在信息科學技術(shù)大樓舉辦， 2007年度圖靈獎獲得者愛德蒙·克拉克教授“巔峰對話”。
圖為愛德蒙·克拉克演講。研通社記者 王皓冉 攝
愛德蒙·克拉克簡單介紹了自己的學術(shù)歷程和主要學術(shù)成果。愛德蒙·克拉克本科期間從事數(shù)學科學專業(yè)，1967年從弗吉尼亞大學獲得數(shù)學學士學位。出于對計算機的酷愛，博士研究期間他選擇了另一個專業(yè)——計算機專業(yè)。本科期間的學習為后來的研究打下了堅實的數(shù)學基礎(chǔ)，從自己感興趣的領(lǐng)域——推理和可計算實數(shù)出發(fā)，他首先著手于實數(shù)的非線性問題。1981年，愛德蒙·克拉克與自己的博士生首次提出模型檢測的想法，并用在自動機并發(fā)系統(tǒng)的驗證研究上，主要使用SAT驗證完成模型檢測，主要針對于有界模型。然而從理論推導到實際工程應(yīng)用是有距離的，因為實際系統(tǒng)大多都是混合系統(tǒng)，尤其是數(shù)值方法直接的使用會出現(xiàn)許多錯誤。為此，愛德蒙教授的團隊針對他們的思想開發(fā)出了dReal實用工具，該工具主要利用DPLL、間隔算法、限制性算法等思想研究實際問題。實際中，信息物理系統(tǒng)是一個龐大的系統(tǒng)，對于系統(tǒng)安全性問題的研究至關(guān)重要。針對這一研究目標，愛德蒙團隊驗證了卡普了猜想，無人駕駛汽車，心臟模擬仿真等問題。
圖為同學們與愛德蒙·克拉克交流。研通社記者 王皓冉 攝
學術(shù)報告結(jié)束后，現(xiàn)場學生與愛德蒙·克拉克開始“對話”環(huán)節(jié)。同學針對專業(yè)問題、科研心得等與愛德蒙·克拉克進行了交流。
有同學對愛德蒙·克拉克提到的“空間爆炸”問題非常感興趣，愛德蒙·克拉克對此作了進一步解釋。他指出，“空間爆炸”可以理解成并行運行過程中進程突然被阻斷的過程，這一過程在計算機應(yīng)用方面有廣泛應(yīng)用，例如微軟設(shè)備驅(qū)動就是一個例子。也有同學大膽質(zhì)疑，愛德蒙·克拉克的模型檢測思想怎樣證明自身的正確性，以及為什么應(yīng)用于軟件系統(tǒng)會比較困難。愛德蒙·克拉克解釋到，自身正確性的檢驗需要一定的抽象程度，一般通過一些編譯器來自檢；而相比于硬件系統(tǒng)，軟件系統(tǒng)有較為復雜的數(shù)據(jù)結(jié)構(gòu)，因此會使得工作量較大。
與純學術(shù)的交流相比，很多同學對于愛德蒙·克拉克的科研經(jīng)驗非常感興趣。關(guān)于如何保持對科研的積極心態(tài)，愛德蒙·克拉克說，自己的性格里對于喜歡的東西有一種著了魔的熱情，喜歡拼盡全力解決問題；時間安排上會給科研工作留出充足的余量，避免自己過度陷入行政工作中。對于如何訓練自己的學生，愛德蒙·克拉克強調(diào)了兩個詞：多自由度和適時引導。他會給自己的學生充足的自由環(huán)境，在此基礎(chǔ)之上加以適度的引導，并著力培養(yǎng)他們專注于探索問題的品質(zhì)。有同學問到教授如何看待數(shù)學基礎(chǔ)訓練的意義，愛德蒙·克拉克給出這樣的回答：計算本身是一件令人興奮的事情，數(shù)學則是做好計算機科學的關(guān)鍵，數(shù)學的各種算法本質(zhì)上是培養(yǎng)一種思維方式，這對于本科生無疑是很好的一個專業(yè)。
圖為校研究生會主席劉博涵代表清華學子向愛德蒙·克拉克贈送禮物。 研通社記者 王皓冉 攝
活動結(jié)束前，清華大學研究生會主席劉博涵代表同學向愛德蒙·克拉克贈送了禮物，愛德蒙·克拉克表示非常高興來到清華大學，有機會跟同學們近距離地交流，他對清華的學生給予了高度評價，認為清華人非常聰明和出色，合作意識也很好，他希望還有機會與清華學生做更進一步的交流。
圖為活動現(xiàn)場。 研通社記者 王皓冉 攝
活動結(jié)束之后，來自電子系的博士生毛洪亮表示，愛德蒙·克拉克自身不論是為人還是學術(shù)都非常嚴謹，今天有幸聽到教授的科研經(jīng)驗，受益頗豐；也有同學對愛德蒙·克拉克的坦承和寬容做出了高度評價，“當我問愛德蒙教授 ‘模型檢測’的局限性時，他說這個思想不是萬能的，有很多領(lǐng)域的問題還沒辦法以此解決；同時針對同行其他專家研究成果，他的評述總是報以包容和支持的態(tài)度。”也有同學表示在這一場論壇中收獲了很多前沿的知識，論壇氛圍非常自由，通過大師的鼓勵獲得了很多正能量，并表示學生學習要崇尚自主學習。
相關(guān)鏈接：
愛德蒙·克拉克（Edmund Clarke）生于1945年，1967年從弗吉尼亞大學獲得數(shù)學學士學位。1976年，康奈爾大學計算機系獲得其博士學位。1981年，他與自己的博士生Allen Emerson首次提出模型檢測（model checking）的想法并用在 自動及并發(fā)系統(tǒng)的驗證研究上。2007年度圖靈獎授予Edmund M.Clarke、E Allen Emerson和Joseph Sifakis三位科學家，表彰他們開發(fā)模型檢測技術(shù)，并使之成為一個廣泛應(yīng)用在硬件和軟件工業(yè)中非常有效的算法驗證技術(shù)所做的奠基性貢獻。
編輯：范 麗
