close

Edmund-Clarke-1608822154.jpg

CMU校長Farnam Jahanian表示,隨著Clarke先生的去世,世界失去瞭計算機科學領域的一位巨人。

上世紀80年代早期,Clarke和他的哈佛大學研究生E. Allen Emerson以及格勒諾佈爾大學的Joseph Sifakis開發瞭模型檢查,這在很大程度上幫助提高瞭復雜計算機芯片、系統和網絡的可靠性。

鑒於這幾位科研人員的工作,計算機協會在2007年給這三位科學傢頒瞭著名的A.M.圖靈獎--被稱之為計算機科學界的諾貝爾獎。

Clarke在發表在Turing Award網站上的獲獎感言中表示,微軟和英特爾等公司都會使用模型檢查來驗證他們計算機網絡和軟件的設計。

根據CMU的說法,模型檢查可以讓工程師分析設計背後的邏輯。它會將硬件或軟件設計的每一種可能狀態考慮在內並確定其是否符合設計者的規格。

CMU指出,在開發模型檢查之前,工程師則都是通過運行模擬測試性能以及手工檢查每一行計算機代碼來檢查計算機電路或軟件程序中的邏輯錯誤。但隨著計算機變得越來越復雜,這些方法變得不夠充分,這使得錯誤往往需要到產品發佈後才被發現。

Clarke則是於1982年加入CMU的計算機科學系。1995年,他成為瞭該校計算機科學學院的第一位講席教授--FORE Systems Professorship。

而在來到CMU之前,Clarke曾在杜克大學和哈佛大學任教。他於1967年獲得弗吉尼亞大學數學學士學位,1968年獲得杜克大學數學碩士學位,1976年獲得康奈爾大學計算機科學博士學位。

另外,Clarke還是《Formal Methods in Systems Design》雜志的前任主編,也是Computer Aided Verification大會的創始人之一。

現在,黎巴嫩山的 Laughlin紀念教堂正在安排私人葬禮。

arrow
arrow
    全站熱搜
    創作者介紹
    創作者 Ken641228 的頭像
    Ken641228

    Ken641228的部落格

    Ken641228 發表在 痞客邦 留言(0) 人氣()