0
  • 聊天消息
  • 系統(tǒng)消息
  • 評論與回復(fù)
登錄后你可以
  • 下載海量資料
  • 學(xué)習在線課程
  • 觀看技術(shù)視頻
  • 寫文章/發(fā)帖/加入社區(qū)
會員中心
創(chuàng)作中心

完善資料讓更多小伙伴認識你,還能領(lǐng)取20積分哦,立即完善>

3天內(nèi)不再提示

2007年圖靈獎得主愛德蒙·克拉克因感染新冠肺炎不幸去世

算法與數(shù)據(jù)結(jié)構(gòu) ? 來源:新智元 ? 作者:新智元 ? 2021-01-14 10:36 ? 次閱讀

【導(dǎo)讀】2007年圖靈獎得主愛德蒙·克拉克(Edmund M. Clarke)因感染新冠肺炎于當?shù)貢r間12月22日不幸去世。

當?shù)貢r間12月22日,2007年圖靈獎得主愛德蒙·克拉克(Edmund M. Clarke)因感染新冠肺炎不幸去世,享年75歲。

他的兒子James Clarke在推特上發(fā)布了這一消息。在推文中,James Clarke說:「今天,我的父親愛德蒙·M·克拉克因為新冠肺炎去世了。他是2007年圖靈獎獲得者。父親對我的學(xué)術(shù)研究一直寄予厚望,他還教我打棒球,釣魚,環(huán)球旅行。我將會深切懷念他?!?/p>

據(jù)了解,James Clarke目前擔任英特爾量子硬件研究組總監(jiān)。

克拉克教授生前一直專注于軟硬件系統(tǒng)的驗證和自動理論證明方面的研究工作。在他的博士論文中,有一項工作就是證明在一些程序語言的控制邏輯中沒有一個完善的Hoare理論證明系統(tǒng)。

教授生平

愛德蒙·克拉克生于1945年,1967年從弗吉尼亞大學(xué)獲得數(shù)學(xué)學(xué)士學(xué)位。1976年,康奈爾大學(xué)計算機系獲得其博士學(xué)位。

1982年,克拉克教授加入卡內(nèi)基梅隆大學(xué)計算機科學(xué)系;在此之前,他先后在杜克大學(xué)和哈佛大學(xué)任教,在那里,他的研究小組繼續(xù)開創(chuàng)形式驗證和自動定理證明。

他是計算機輔助驗證會議的創(chuàng)始人之一,也曾擔任過Formal Methods in Systems Design雜志的主編。

1995年,克拉克成為第一個獲得FORE Systems教授資格的人,2008年,他升任大學(xué)教授,這也是CMU教師的最高榮譽。

他曾獲得1998年的ACM Kanellakis獎,1999年Allen Newell 研究卓越獎,2004年 IEEE Harry h. Goode 紀念獎以及2008年自動推理演繹會議Herbrand杰出貢獻獎(共同獲得者)。2014年,富蘭克林學(xué)會授予他鮑爾科學(xué)成就獎,以表彰他在計算機系統(tǒng)驗證技術(shù)的構(gòu)想和開發(fā)方面的領(lǐng)導(dǎo)作用。

他在2015年當選CMU名譽教授。

教計算機自己檢查錯誤的人走了

自計算機誕生以來,工程師們通過運行模擬以測試性能或手動檢查每行計算機代碼的方法來檢查計算機電路或軟件程序中的邏輯錯誤。但是,隨著計算機芯片上組件的數(shù)量呈幾何級數(shù)增長,軟件和計算機系統(tǒng)同樣也變得更加復(fù)雜,這些偶然的「非正式驗證」方法顯然是不夠的。錯誤通常在產(chǎn)品發(fā)布后才被發(fā)現(xiàn),因為即使是微小的錯誤就整起來也非常昂貴的。

1981年,當時在哈佛擔任助理教授的克拉克與他的研究生E. Allen Emerson以及Grenoble大學(xué)的Joseph Sifakis,開發(fā)了一種自動檢測計算機硬件和軟件設(shè)計錯誤的方法,被稱為模型檢測。

模型檢測是一種分析設(shè)計背后邏輯的「形式驗證」,就像數(shù)學(xué)家使用證明來確定一個定理是正確的。模型檢測考慮硬件或軟件設(shè)計的每一種可能狀態(tài),并確定它是否與設(shè)計者的規(guī)范一致,大大避免了偶然錯誤的出現(xiàn),隨后它被廣泛應(yīng)用,幫助提高復(fù)雜計算機芯片、系統(tǒng)和網(wǎng)絡(luò)的可靠性。

克拉克教授和E. Allen Emerson, Joseph Sifakis因此獲得了2007年的圖靈獎。

卡內(nèi)基梅隆大學(xué)的校長Farnam Jahanian說:「Ed在模型檢測方面的開創(chuàng)性工作將形式化的計算方法應(yīng)用于最終的挑戰(zhàn): 計算機檢查自己的正確性。隨著系統(tǒng)變得越來越復(fù)雜,我們才剛剛開始看到Ed的見解所帶來的廣泛和長期的益處,這將在未來幾年繼續(xù)激勵研究人員和實踐者。」

新冠帶走了克拉克教授,從此世界又少了一個計算機巨人,但天堂沒有新冠,教授,走好!

責任編輯:lq

聲明:本文內(nèi)容及配圖由入駐作者撰寫或者入駐合作網(wǎng)站授權(quán)轉(zhuǎn)載。文章觀點僅代表作者本人,不代表電子發(fā)燒友網(wǎng)立場。文章及其配圖僅供工程師學(xué)習之用,如有內(nèi)容侵權(quán)或者其他違規(guī)問題,請聯(lián)系本站處理。 舉報投訴
  • 計算機科學(xué)
    +關(guān)注

    關(guān)注

    1

    文章

    144

    瀏覽量

    11380
  • 圖靈獎
    +關(guān)注

    關(guān)注

    0

    文章

    5

    瀏覽量

    2094
  • 控制邏輯
    +關(guān)注

    關(guān)注

    0

    文章

    14

    瀏覽量

    2356

原文標題:巨星隕落!圖靈獎得主Edmund Clarke感染新冠逝世,教計算機自己檢查錯誤的人走了

文章出處:【微信號:TheAlgorithm,微信公眾號:算法與數(shù)據(jù)結(jié)構(gòu)】歡迎添加關(guān)注!文章轉(zhuǎn)載請注明出處。

收藏 人收藏

    評論

    相關(guān)推薦

    邵逸夫獎得主圓桌論壇于香港科學(xué)館舉行

    ?科學(xué)的未來:突破與影響 香港202411月15日?/美通社/ --?“邵逸夫獎得主圓桌論壇-科學(xué)的未來:突破與影響”由邵逸夫獎基金會和香港科學(xué)館聯(lián)合主辦,并由南華早報籌劃,11月14日(星期四
    的頭像 發(fā)表于 11-16 13:30 ?270次閱讀
    邵逸夫<b class='flag-5'>獎得主</b>圓桌論壇于香港科學(xué)館舉行

    Meta震撼發(fā)布Orion AR眼鏡:重塑未來計算平臺

    克拉克·肯特經(jīng)典黑色鏡框設(shè)計的AR眼鏡,雖看似平凡,實則蘊含著Meta創(chuàng)始人扎伯格對未來計算平臺變革的深遠布局與數(shù)十億美元的豪賭。
    的頭像 發(fā)表于 09-26 16:17 ?1058次閱讀

    圖靈測試的內(nèi)容是什么_圖靈測試的作用

    圖靈測試(Turing Test)是由英國數(shù)學(xué)家和計算機科學(xué)家艾倫·麥席森·圖靈(Alan Turing)在1950提出的一種測試方法,用以判斷機器是否具有人類智能。圖靈測試的核心內(nèi)
    的頭像 發(fā)表于 09-16 16:11 ?2218次閱讀

    圖靈測試什么意思_圖靈測試是干嘛的

    圖靈測試是由英國數(shù)學(xué)家、密碼專家和數(shù)字計算機的奠基人艾倫·麥席森·圖靈提出的一種檢驗?zāi)硞€對象(通常是機器或人工智能系統(tǒng))是否具有智能的測試方法。其核心思想在于,如果一臺機器在與人類的對話過程中,能夠使得測試者無法區(qū)分其是人還是機器,那么就可以認為這臺機器具備了智能。
    的頭像 發(fā)表于 09-16 16:09 ?1791次閱讀

    利用vMeasure eMobilityAnalyzer函數(shù)庫分析電機性能

    本文利用vMeasure eMobilityAnalyzer函數(shù)庫中的克拉克變換功能,將三相電機定子電流或電壓轉(zhuǎn)換為兩相電流或電壓,幫助工程師更有效地、可視化地分析電機的行為并對控制算法進行針對性的優(yōu)化,從而提高電機的性能和效率。
    的頭像 發(fā)表于 09-13 11:37 ?426次閱讀
    利用vMeasure eMobilityAnalyzer函數(shù)庫分析電機性能

    耐能聯(lián)合創(chuàng)始人喜獲首屆亞裔美國先鋒獎?wù)?/a>

    (Steven Chu)和蘭迪·謝曼(Randy Schekman)以及圖靈獎得主拉杰·雷迪(Raj Reddy)將發(fā)表主題演講,前斯坦福大
    的頭像 發(fā)表于 07-31 10:30 ?498次閱讀

    羅杰·瑞迪:AI能力已遠超我們?nèi)祟?/a>

    在科技日新月異的今日,人工智能(AI)正以前所未有的速度重塑著我們的世界,其影響力之深廣,已遠遠超出了最初的想象。2024世界人工智能大會上,圖靈獎得主羅杰·瑞迪的一席話,如同警鐘長鳴,他深刻指出
    的頭像 發(fā)表于 07-05 14:10 ?373次閱讀

    國芯科技與圖靈量子簽署戰(zhàn)略合作協(xié)議

    近日,蘇州國芯科技股份有限公司(以下簡稱“ 國芯科技 ”,股票代碼 688262.SH )與上海圖靈智算量子科技有限公司(以下簡稱“ 圖靈量子 ”)簽署戰(zhàn)略合作協(xié)議,雙方達成業(yè)務(wù)合作共識,共同研究基于 量子技術(shù)的信創(chuàng)和信息安全產(chǎn)品迭代方案 。
    的頭像 發(fā)表于 06-15 17:22 ?1515次閱讀

    光刻巨人去世 阿斯麥(ASML)光刻機巨頭聯(lián)合創(chuàng)始人去世

    圈內(nèi)突發(fā)噩耗,光刻巨人去世; 阿斯麥(ASML)光刻機巨頭聯(lián)合創(chuàng)始人維姆?特羅斯特去世。 據(jù)外媒報道,在當?shù)貢r間11日晚,荷蘭光刻機巨頭阿斯麥(ASML)創(chuàng)始人之一維姆?特魯斯特(Wim
    的頭像 發(fā)表于 06-13 15:13 ?7029次閱讀

    戴爾預(yù)測DRAM與固態(tài)硬盤下半年價格將持續(xù)上漲

    在全球科技產(chǎn)業(yè)中,戴爾一直以其精準的市場洞察和卓越的供應(yīng)鏈管理能力而著稱。然而,在近期舉行的2025財年第一季度財報電話會議上,戴爾首席運營官杰弗里?克拉克(Jeffrey Clarke)卻發(fā)出了一個令人關(guān)注的警告:下半年DRAM內(nèi)存和固態(tài)硬盤的價格將持續(xù)上漲。
    的頭像 發(fā)表于 06-05 10:17 ?553次閱讀

    用DOCA實現(xiàn)3D打印工廠智能化數(shù)據(jù)處理

    “國寶”是本次活動的三等獎得主,作為增材制造(3D 打印)、智能制造的工業(yè)互聯(lián)網(wǎng)領(lǐng)域的產(chǎn)品經(jīng)理,他擅長利用最新的 AI 技術(shù)解決行業(yè)中的問題。
    的頭像 發(fā)表于 04-15 09:52 ?351次閱讀

    了解幾位發(fā)明天線的先驅(qū)

    1864左右,蘇格蘭物理學(xué)家詹姆斯·克拉克·麥克斯韋(James Clerk Maxwell)提出了無線電理論。
    發(fā)表于 03-28 13:54 ?938次閱讀
    了解幾位發(fā)明天線的先驅(qū)

    捷科技發(fā)布2023度業(yè)績快報 凈利暴漲220.19%!

    WitDisplay消息,3月11日,捷科技發(fā)布2023度業(yè)績快報。
    的頭像 發(fā)表于 03-13 14:25 ?851次閱讀
    <b class='flag-5'>冠</b>捷科技發(fā)布2023<b class='flag-5'>年</b>度業(yè)績快報 凈利暴漲220.19%!

    【RISC-V開放架構(gòu)設(shè)計之道|閱讀體驗】學(xué)習處理器體系架構(gòu)的一本好書

    Patterson是圖靈獎得主,在計算機行業(yè)中極具影響力,他參與主編的多本教材是計算機體系結(jié)構(gòu)、計算機組成原理等相關(guān)課程的知名教材,我在日常教學(xué)中經(jīng)常推薦給學(xué)生閱讀。該書的另一位作者是安德魯·沃特曼
    發(fā)表于 01-23 20:08

    玄鐵的rv64ilp32之路 - 32位Linux的未來

    計算機科學(xué)巨擘、圖靈獎得主唐納德在2008的博客中曾發(fā)表過一段著名的言論,他抱怨道:在編譯內(nèi)存需求不足4GB的程序時,使用64位指針是非常不明智的。因為當這些指針值出現(xiàn)在結(jié)構(gòu)體中時
    的頭像 發(fā)表于 01-23 16:25 ?2187次閱讀
    玄鐵的rv64ilp32之路 - 32位Linux的未來