金磊 發自 凹非寺
量子位 報導 | 公眾號 QbitAI
又一位巨星隕落！
據最新消息，2007年圖靈獎得主、計算機科學家Edmund Clarke，因感染新冠肺炎，於北京時間12月23日上午不幸逝世。
其子James S. Clarke在Twitter發文公布此消息之餘，也悼念道：
雖然他對（我）學業上的成功總是抱有很高的期望，但他也教會了我打棒球、釣魚和環遊世界。
我將深深地懷念他。
對此，中國科學院大學教授包雲崗表示：
享年75歲，人類的損失！
網友們在表達哀悼的同時，也給予了Edmund高度的認可：
如果沒有他的貢獻，很難想像我的領域會是什麼樣子。
他對科學的貢獻是無法估量的。
Edmund Clarke：「軟體和硬體驗證」先驅
Edmund出生於1945年7月27日。
根據維基百科的介紹，他於1967年維吉尼亞大學獲得數學學士學位；次年，在杜克大學拿到了數學碩士學位。
1976年，Edmund於康奈爾大學獲得了計算機科學博士學位。
此後，他先是在杜克大學計算機科學系任教2年，並於1978年轉到了哈佛大學，擔任應用科學系計算機科學助理教授。
1982年，離開哈佛大學的他，又來到了卡內基梅隆大學計算機科學系任教。
7年後，也就是1989年，Edmund 被任命為正教授。
值得注意的是，他是CMU計算機科學學院FORE Systems Professorship的第一位獲得者。
根據維基百科所述，Edmund所擅長的研究包括「軟體和硬體驗證」以及「自動定理證明」。
早在他的博士論文中，便證明了：
某些程式語言控制結構沒有良好的Hoare式證明系統。
1981年，Edmund和他的博士生E. Allen Emerson，首次提出使用模型檢查作為有限狀態並發系統的驗證技術。他的研究小組率先將模型檢查用於硬體驗證。
使用二元決策圖（binary decision diagram）的符號模型檢查，也是由他的研究小組開發。
這一重要技術是Kenneth McMillan的博士論文的主題，該論文還獲得了ACM博士論文獎。
此外，他的研究小組還開發了第一個並行解析定理推理器（Parthenon）和第一個基於符號計算系統的定理推理器（Analytica）。
2007年，他與Ernest Allen Emerson和Joseph Sifakis一起，因在模型檢查方面取得的傑出貢獻而獲得圖靈獎。
也正因Edmund在該領域中的傑出貢獻，他還斬獲了ACM Paris Kanellakis獎、赫布蘭獎、美國國家工程院院士等榮譽和頭銜。
Edmund還是中國科學院「愛因斯坦講席教授」，在2013年10月在中國科學院進行過訪問交流。
△圖源：中國科學軟體研究所
其他巨星的隕落
對計算機領域做出如此傑出貢獻者，因疫情而逝世實屬令人惋惜。
這無疑是「人類的損失」。令人更為痛心的是，回看「黑天鵝」襲來的這一年，還有太多因新冠而隕落的巨星。
4月12日，當代最有趣的數學家John Horton Conway，因為新冠肺炎逝世，享年82歲。
有人評價他，世界上可能有比他更厲害的數學家，但是在頂尖的數學家裡，沒有人能比他科普做得更好。
他在數學領域多點開花，是一個在組合博弈論、幾何、數論、群論、算法甚至量子力學理論等多個方面都做出貢獻的天才數學家。
2月15日，華中科技大學教授、中國工程院院士著名機械工程專家段正澄因感染新冠肺炎去世，享年86歲。
段院士生前一直工作在一線，與生產緊密結合，致力於國家重要需求的自動化、數位化加工技術與裝備的應用基礎研究和工程技術研發。
段院士獲得過國家科學技術進步一等獎1項、二等獎3項。其中二等獎的3項成果，沒有哪一項少於10年：
研製全身伽瑪刀，10年；研究雷射加工技術與裝備，20年；完善汽車發動機曲軸磨床，30年。
……
他們對科學、對人類所創造出來的價值，用「無價」來形容並不為過。
應當值得被後人謹記和尊重，不僅僅是卓越的貢獻和事跡，更是他們所秉持的對科學的精神。
參考連結：
https://zh.wikipedia.org/wiki/%E7%88%B1%E5%BE%B7%E8%92%99%C2%B7%E5%85%8B%E6%8B%89%E5%85%8B#cite_note-2
https://twitter.com/Jim_in_Oregon/status/1341546882321944576
http://www.iscas.ac.cn/xwdt2016/kjdt2016/201310/t20131022_3960865.html
— 完 —
本文系網易新聞•網易號特色內容激勵計劃籤約帳號【量子位】原創內容，未經帳號授權，禁止隨意轉載。
原標題：《又一位巨星因「新冠」隕落，07年圖靈獎得主Edmund Clarke，享年75歲》
閱讀原文