自動驗證技術獲得圖靈獎

三人分享圖靈獎

正當我們忙于抗震救災和準備奧運的時候，2008年6月21日晚，美國計算機協會(ACM)在舊金山召開了2007年度ACM頒獎盛典。頒布了2007年度圖靈獎、ACM Infosys基金會獎以及人工智能、軟件系統、計算機理論與實踐、計算科學與工程等領域的多個獎項。

2007年度ACM圖靈獎由三位研究人員分享，分別是卡內基·梅隆大學的Edmund M.Clarke教授、德克薩斯大學奧斯汀分校的E.AllenEmerson教授和法國Grenoble大學Verimag實驗室的Joseph Sifakis教授，獎金是由英特爾公司和谷歌公司共同提供的25萬美元，以表彰他們“在將模型檢測發展為硬件和軟件業中廣泛采用的高效驗證技術上的貢獻”。

自動驗證用途廣

今天，軟件、硬件、網絡的規模越來越大，例如一個芯片上就有上億個晶體管電路，一個嵌入式系統雖小，也五臟俱全。如果設計出了問題，一旦投產，損失就相當大。如何在設計時就能證明系統正確，或者如何能及時發現設計中的錯誤呢?

目前，一種成效卓著的自動驗證技術(Automatic Verification Technology)已經在硬件和軟件工業界得到了廣泛的應用，特別是在半導體芯片的設計與生產中得到成功的應用。正如英特爾研究中心副總裁錢安達(AndrewChien)在評價模型檢測技術時所說：“英特爾和整個計算機工業都從他們的貢獻中直接獲益”。谷歌的高級工程副總裁Alan Eustace也說：“谷歌像其他同時代的技術公司一樣，很大一部分成功都來自于先驅們的研究貢獻”。這些祝賀與評價充滿了真誠的感激之情。

模型檢測是核心

所謂模型檢測技術(ModelCheeking)，本質上是用嚴密的數學方法來驗證一個設計是否滿足預先設定的需求，從而自動地發現設計中的錯誤?！?br>