哀悼!2007年圖靈獎得主Edmund Clarke因感染新冠逝世
2020年12月23日18:16

  來源:AI科技評論

  作者/陳彩嫻、陳大鑫

  AI科技評論最新消息,當地時間12月23日,2007年圖靈獎得主Edmund M. Clarke(愛德蒙·克拉克)因感染新冠肺炎不幸去世。

  其子James S. Clarke隨後發推文緬懷父親:“他對我的學術研究有著極高的期望,同時又教我打棒球、釣魚,以及環遊世界。我將深深地銘記他。”

  在父親的影響下,James在學業上也取得了卓越的成就,於1999年獲得哈佛大學物理化學博士學位,目前任職英特爾量子硬件研究組總監。

  Edmund出生於1945年,1967年從維珍尼亞大學獲得數學學士學位,1968年從杜克大學獲得數學碩士學位,1976年從維珍尼亞大學獲得計算機博士學位。

  博士畢業後,Edmund先是在杜克大學任教兩年。隨後,1978年,他加入哈佛大學擔任助理教授。1982年,Clarke離開哈佛,加入卡內基梅隆大學計算機系,並在1989年被評為全職終身教授。

  Edmund一直專注於軟硬件系統的驗證和自動理論證明方面的研究工作。在他的博士論文中,有一項工作就是證明在一些程式語言的控制邏輯中沒有一個完善的Hoare理論證明系統。

  1981年,他與門下的博士生Allen Emerson首次提出模型檢測(model checking)的觀點,並將其用在自動及併發系統的驗證研究上。他們使用SAT驗證完成模型檢測,主要針對有界模型。

  然而,從理論推導到實際工程應用仍有一定差距,因為實際系統大多是混合系統,而且直接使用數值方法會出現許多錯誤。為此,Edmund與團隊成員開發了dReal實用工具,利用DPLL、間隔算法、限製性算法等思想研究實際問題。

  2007年,Edmund與E Allen Emerson、Joseph Sifakis等兩位科學家一同獲得圖靈獎,獲獎理由是他們開發了模型檢測技術,並使之成為廣泛應用於硬件和軟件工業里的有效算法驗證技術。

  2013年,Edmund曾參加了清華大學的“巔峰對話”活動,席間介紹了自己的學術曆程與主要學術成果。他提到,本科期間的學習為他後來的研究打下了堅實的數學基礎。他從自己感興趣的推理和可計算實數出發,著手於實數的非線性問題研究。

  對於如何保持積極的科研心態,Edmund表示:自己對於喜歡的事物有一種著魔般的熱情,喜歡拚盡全力解決問題;在時間安排上,他會給科研工作留出充足的時間,避免自己過度陷入繁瑣的行政工作中。

  對於如何培養學生,Edmund強調了兩個詞:充分的自由與適時的引導。他會給自己的學生一個自由的研究環境,在此基礎上加以適度的引導,並著力培養他們專注於探索問題的品質。

  至於如何看待數學基礎訓練的意義,Edmund認為:計算本身就是一件令人興奮的事情,而數學是學好計算機科學的關鍵,學習數學的各種算法本質上就是培養一種思維方式,因此,本科生學習數學是很好的。

關注我們Facebook專頁
    相關新聞
      更多瀏覽