圖靈獎得主克拉克感染新冠逝世 圖靈獎得主愛德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸去世，享年75歲。他的兒子 James Clarke （英特爾量子硬件研究組總監(jiān)）在推特上發(fā)布了這一消息。

自計算機誕生以來，工程師們通過運行模擬以測試性能、或者手動檢查每行計算機代碼的方法來檢查計算機電路或軟件程序中的邏輯錯誤。

但是，隨著計算機芯片上組件的數(shù)量呈幾何級數(shù)增長，軟件和計算機系統(tǒng)同樣也變得更加復(fù)雜，這些偶然的「非正式驗證」方法顯然是不夠的。

錯誤通常在產(chǎn)品發(fā)布后才被發(fā)現(xiàn)，因為即使是微小的錯誤就整起來也非常昂貴的。

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

模型檢測是一種分析設(shè)計背后邏輯的「形式驗證」，就像數(shù)學(xué)家使用證明來確定一個定理是正確的。

模型檢測考慮硬件或軟件設(shè)計的每一種可能狀態(tài)，并確定它是否與設(shè)計者的規(guī)范一致，大大避免了偶然錯誤的出現(xiàn)，隨后它被廣泛應(yīng)用，幫助提高復(fù)雜計算機芯片、系統(tǒng)和網(wǎng)絡(luò)的可靠性。