計算機巨星隕落!圖靈獎得主 Edmund Clarke 逝世

2021-02-18 IT有得聊

"IT有得聊」是機械工業出版社旗下IT專業資訊和服務平臺，致力於幫助讀者在廣義的IT領域裡，掌握更專業、實用的知識與技能，快速提升職場競爭力。 點擊藍色微信名可快速關注我們！

本以為歷經波折的 2020 年即將畫上句號，可在尾聲，我們又獲知了一個不幸的消息：12 月 23 日，英特爾量子硬體研究組總監 James S. Clarke 在推特發布訃告，他的父親、2007 年圖靈獎得主 Edmund M. Clarke 因感染新冠不幸去世，享年 75 歲。

Edmund M. Clarke ，這位「模型檢測先驅」，他這 75 年的人生，為科技的貢獻無法計量。

01

生平經歷

Edmund M. Clarke 出生於 1945 年，1967 年獲得維吉尼亞大學的數學學士學位，1968 年在杜克大學取得數學碩士學位，隨後，又於 1976 年在康奈爾大學獲得計算機博士學位。

完成學業後， Edmund M. Clarke 開始了他的職業生涯。1976 年，他在杜克大學任教 2 年，後於 1978 年在哈佛大學擔任助理教授，1982 年加入卡內基梅隆大學計算機系，並於 1989 年被評為全職終身教授一職。隨後在 1995 年，他成為了卡內基梅隆大學計算機科學學院 FORE Systems Professorship 的第一位獲獎者。

Edmund M. Clarke 生平獲獎如數

據其個人博客介紹，Edmund M. Clarke 生平的興趣涵蓋三個領域：編程系統，硬體和理論。他使用理論計算機科學領域的技術來解決編程系統和硬體設計中的實際問題。在過去的30多年中，重點研究模型檢測以及硬體和軟體正確性的形式驗證。

他的生平經歷已足夠優秀，而他的科技成就更加輝煌。

02

著名的模型檢測

其實談起 Edmund M. Clarke ，了解的人腦海裡浮現的第一印象大概就是「模型檢測」吧。

1981 年， Edmund M. Clarke 和他的博士生 E. Allen Emerson 首次提出了模型檢測 (model checking) 概念，並主張可作為自動機並發系統的驗證技術，隨後率先將其應用在了硬體驗證上。

2004 年， Edmund M. Clarke 獲得 IEEE 計算機學會 Harry H. Goode 紀念獎，以表彰他對硬體和軟體系統形式驗證做出的重大開創性貢獻。

2007 年的圖靈獎（圖靈獎旨在獎勵對計算機事業作出重要貢獻的個人 ，獲獎條件要求極高，評獎程序極嚴，一般每年僅授予一名計算機科學家。）為表彰模型檢測技術的開發，授予 Edmund M. Clarke、E Allen Emerson 和 Joseph Sifakis 三位科學家，這也使得模型檢測成為一個廣泛應用在硬體和軟體工業中非常有效的算法驗證技術所做的奠基性貢獻。

此外，Edmund M. Clarke 在 2008 年獲得了 Herbrand 獎，以「表彰他在模型檢測的發明中所發揮的作用，以及他在該領域20多年來的持續領導地位」。在 2014 年他又因為模型檢測獲得了鮑爾獎和科學成就獎。

模型檢測作為自動驗證技術，通過顯式狀態搜索或隱式不動點計算來驗證有窮狀態並發系統的模態/命題性質。由於模型檢測可以自動執行，並能在系統不滿足性質時提供反例路徑，因此在工業界比演繹證明更受推崇。目前，模型檢測已被廣泛應用於計算機硬體、通信協議、控制系統、安全認證協議等方面的分析與驗證中，不僅在學術領域熠熠生輝，在產業界也取得了成功的發展。

03

眾人悼念！

Edmund M. Clarke 的逝世，引起了許多人的嘆息。

Edmund M. Clarke 的兒子， 英特爾量子硬體研究組總監 James S. Clarke 在告知大眾這個不幸的消息時，也訴說了他的思念：

父親對我的學術研究總是抱有很高的期望，但他也教會了我如何打棒球、釣魚，並帶我到世界各地旅行，我將永遠懷念他。

中國科學院計算技術研究所研究員、博士生導師、所長助理包雲崗，對 Edmund M. Clarke 的離世表示哀悼：

Edmund M. Clarke 曾經的學生、威斯康辛大學麥迪遜分校教授在得知恩師去世的消息後，也在推特上表示：2020 年不能再糟糕了。


除此之外，許多網友也對此表示惋惜：

他在模型檢查和自動定理證明方面的工作，塑造了許多計算世界能夠可靠運行的方式，他的貢獻成為永久的遺產。


聽到這個消息我非常難過。他是我們這個領域的巨人，Edmund 和他的作品將被永遠銘記，並將繼續影響和塑造我們的領域。

Edmund M. Clarke ，這位計算機領域「巨人」，他所創造的價值、帶來的影響對於我們來說可謂「無價」，他將永遠銘記於我們的心中，一路走好.


-End-

相關焦點

  • 又一位巨星因「新冠」隕落,07年圖靈獎得主Edmund Clarke,享年75歲
    金磊 發自 凹非寺量子位 報導 | 公眾號 QbitAI又一位巨星隕落！據最新消息，2007年圖靈獎得主、計算機科學家Edmund Clarke，因感染新冠肺炎，於北京時間12月23日上午不幸逝世。
  • 2007圖靈獎得主離開了:模型檢測先驅Edmund Clarke因新冠逝世
    Clarke 發文表示，他的父親、2007 年圖靈獎得主 Edmund M. Clarke 因感染新冠不幸去世，享年 75 歲。Edmund M. Clarke 生前就職於卡內基梅隆大學（CMU），是該校的終身教授。
  • 巨星隕落!07年圖靈獎得主Edmund Clarke因感染新冠逝世
    當地時間12月23日，2007年圖靈獎得主Edmund M． Clarke（愛德蒙·克拉克）因感染新冠肺炎不幸去世，享年75歲。其子James S． Clarke隨後發推文緬懷父親：「他對我的學術研究有著極高的期望，同時又教我打棒球、釣魚，以及環遊世界。
  • 中科院「愛因斯坦講席教授」、圖靈獎得主Edmund Clarke教授訪問...
    美國卡內基梅隆大學計算機系教授、中國科學院「愛因斯坦講席教授」、圖靈獎得主EdmundClarke於10月20日至27日對蘇州研究院進行了為期8天的學術訪問與交流。  Edmund Clarke教授是形式化驗證領域中模型檢查（Model Checking）技術的創始人之一，美國計算機學會（ACM）與美國電氣電子工程師學會（IEEE）院士，同時也是美國國家科學院和工程院院士
  • 享年75歲,圖靈獎得主Edmund Clarke因感染新冠逝世
    公眾號「國外碩博招生」，每天監控國外獎學金多、愛招中國學生的名校招錄信息，千萬別錯過哦，掃碼關注——國外碩博招生當地時間12月23日，2007年圖靈獎得主Edmund M. Clarke（愛德蒙·克拉克）因感染新冠肺炎不幸去世。其子James S.
  • A.M.圖靈獎獲得者、CMU教授Edmund M. Clarke因COVID-19去世
    圖靈獎得主Edmund M. Clarke在長期患病後於當地時間周二死於COVID-19，享年75歲。Clarke來自黎巴嫩山，他最著名的工作成果是模型檢查，這是一種檢測計算機硬體和軟體設計錯誤的自動化方法。CMU校長Farnam Jahanian表示，隨著Clarke先生的去世，世界失去了計算機科學領域的一位巨人。
  • 你一定不知道的12位圖靈獎得主
    後來我再回答這個問題時尾加一句：C語言之父是圖靈獎得主，Java語言之父目前還沒得到這個獎。我發現學生表情有很大的變化.。圖靈獎（Turing Award）於1966年設立，獎勵在計算機領域作出傑出貢獻的個人（1966年至2019年共73名獲獎者）。
  • 最年輕圖靈獎得主:計算機是數學好的女性的完美學科
    這位最年輕的圖靈獎得主觀察到，機器學習和大數據促成了世界範圍內的權力轉移。「看看2001年市值最高的公司，都是通用電氣和埃克森美孚之類的能源企業；2016年都是大數據公司。難怪他們說現在數據就是石油，數據就是貨幣。」那麼，普通人在大數據時代會面臨什麼樣的安全威脅呢？「我覺得什麼都是威脅。」戈德瓦瑟在10月31日接受澎湃新聞專訪時笑道。
  • 悼念圖靈獎得主、ML語言之父Robin Milner
    據外媒消息，1991年圖靈獎得主Robin Milner於2010年3月20日（他妻子葬禮後的第三天）在英國劍橋辭世，享年76歲。他是他是英國皇家學會成員，ACM會士，美國工程院外籍院士。1995年，他回到母校劍橋大學任教，並擔任劍橋大學計算機實驗室主任。（來自維基百科）2005年4月Milner曾經訪問中國。去世前，他的主要研究興趣是模型在普適計算中的系統應用，和偶圖（Bigraphy）模型。貢獻他獲得圖靈獎的主要貢獻是：1.
  • 圖靈獎得主David Patterson為你解惑
    在主論壇上，圖靈獎得主David Patterson將帶來宗師課《體系結構創新加速人工智慧》。人工智慧已經成為新一輪產業變革的核心驅動力，正在對世界經濟、社會進步和人類生活產生極其深刻的影響。在活動期間，大會也將進行上海白玉蘭開源開放研究院揭牌、發布《人工智慧開源開放報告》、WAIC 雲帆獎。在今年的開發日主論壇上，機器之心聯合上海交通大學人工智慧研究院特邀請到了多位重磅嘉賓，其中就包括 2017 年圖靈獎得主、計算機體系結構宗師 David Patterson。
  • 圖靈獎得主教出來的圖靈班到底多牛?
    領銜建立圖靈班的大佬就是約翰·霍普克洛夫特，他是當今世界赫赫有名的頂級計算機科學家。2017年5月，約翰·霍普克洛夫特宣布加入北京大學信息科學技術學院，成為首位入職北大的圖靈獎得主。曼紐爾·布盧姆是第三十屆圖靈獎得主，同時也是卡內基梅隆大學計算機科學教授，美國國家科學院的成員，響噹噹的世界理論計算機學大師。
  • 圖靈、圖靈機、圖靈獎
    1966年由美國計算機協會ACM設「圖靈獎」，是計算機界最負盛名、最崇高的一個獎項，有「計算機界的諾貝爾獎」之稱，每年評選出一名計算機科學家。目前獲得「圖靈獎」的華人學者僅有2000年圖靈獎得主姚期智教授。（已入中國籍）。圖靈對於人工智慧的發展有諸多貢獻，提出了一種用於判定機器是否具有智能的試驗方法，即圖靈試驗，至今，每年都有試驗的比賽。
  • 圖靈獎頒給《玩具總動員》打造者 憑什麼?
    改變一個產業，引領一個時代，獲很多次奧斯卡獎，加冕計算機最高領域——圖靈獎。這就是剛剛出爐的2019圖靈獎得主：Edwin E. Catmull艾德·卡特姆，以及Patrick M. Hanrahan派屈克· 漢拉汗。
  • 放棄外籍身份,中國71歲圖靈獎得主姚期智:我要回去了,永遠的
    姚期智，世界頂級的科學家，在美國享有極高的聲譽，姚期智曾經獲得過計算機科學的諾貝爾獎——圖靈獎，可謂是功成名就。 但是當國家號召海外優秀人才歸國支援中國建設之時，71歲高齡的圖靈獎得主姚期智，毅然決然地放棄了美國的一切，永遠的離開了美國，致力於中國計算機人才的培養。
  • 最新圖靈獎頒布!皮克斯創始人獲獎 引領計算機技術和電影「聯姻...
    圖靈獎獲得者，以表彰他們對3D計算機圖形學的貢獻，以及這些技術對電影製作和計算機生成圖像（computer-generated imagery，CGI）等應用的革命性影響。關於圖靈獎圖靈獎由 ACM 於 1966 年設立，全稱 ACM A.M. 圖靈獎（ACM A.M.Turing Award），旨在獎勵對計算機事業作出重要貢獻的個人。
  • 圖靈獎得主長文報告:是什麼開啟了計算機架構的新黃金十年?(上)
    這種柳暗花明的背後，顯示的正是計算機計算架構的時代變革；新的方法、新的思維、新的目標引領了新的浪潮。2017 年圖靈獎的兩位得主 John L. Hennessy 和 David A. Patterson 就是這個新浪潮的見證者和引領者。
  • 圖靈獎得主David Patterson:將Python重寫為C,性能最高提升1000倍!
    周志華教授是AI領域會士「大滿貫」得主，AAAI 2019程序主席、IJCAI 2021程序主席，《機器學習》一書的作者。  新智元報導  來源：spectrum.ieee.org編譯：李靜怡【新智元導讀】2017年圖靈獎得主
  • 圖靈獎唯一中國得主,成為同濟大學名譽教授
    圖靈獎唯一中國得主，成為同濟大學名譽教授 2020-08-15 15:29 來源：澎湃新聞·澎湃號·湃客
  • 圖靈獎得主大衛·帕特森宣布依託清華-伯克利深圳學院建設RISC-V...
    當地時間6月12日， 圖靈獎得主、計算機體系結構領域享譽世界的頂級科學家大衛·帕特森（David Patterson）在瑞士宣布，將依託清華-伯克利深圳學院（TBSI），建設RISC-V國際開源實驗室（RISC-V International Open Source
  • 2007年圖靈獎得主因感染新冠肺炎去世,享年75歲
    Clarke在社交媒體發文表示，他的父親、2007年圖靈獎得主愛德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸去世。James S. Clarke在社交媒體發文。愛德蒙·克拉克曾任美國卡內基梅隆大學計算機科學系教授，是ACM和IEEE會士。他在軟硬體驗證、自動定理證明、形式方法等方面享有崇高的國際聲譽，是模型檢驗方法的開創者之一。