摘要
又一點陣圖靈獎得主去世了，他是受人尊敬的時序邏輯領域大師艾米爾· 伯努利(AmirPnueli)。今年11月2日，這位1996年度圖靈獎得主因腦出血去世，享年68歲，只剩那些熠熠生輝的科技成就留給後人 。
貢獻
艾米爾·伯努利在計算機出現後的最初幾十年里，計算機實質上是一個巨大的計算器，數字被錄入，計算結果被輸出。直到20世紀70年代，科學家們才意識到需要正確地驗證這些計算結果。隨著電腦變得更強大，軟體更先進，多任務和變化的數據核查變得更加困難。因此，程式設計師不得不考慮到時間推移下系統的行為。在這個契機下，時序邏輯被引入計算科學，這是計算科學發展歷史的重要轉折點。
時序邏輯也叫時態邏輯（temporal logic)，是計算機科學裡一個很專業很重要的領域。時序邏輯被用來描述為表現和推理關於時間限定的命題的規則和符號化的任何系統，主要用於形式驗證。20 世紀60 年代Arthur Prior提出介入的基於模態邏輯的特殊的時間邏輯系統，這一理論後來被艾米爾·伯努利等邏輯學家進一步發展。
後來，Pnueli在史丹福大學和IBM Waston 研究中心從事博士後的研究工作，從這時開始，他將工作研究方向轉移到計算機科學領域。1973年，他創辦了特拉維夫大學計算機科學系，並擔任第一任院長。1977 年，Pnueli開創性地把時態邏輯引入計算機科學，他的時態邏輯是非經典邏輯中的一種，研究如何處理含有時間信息的事件的命題和謂詞。現在通常稱為時序邏輯的計算機系統，就出現在這一年，Pnueli 在子程式語言與系統驗證方面做出的傑出貢獻具有里程碑意義。
“Pnueli實現了這一邏輯，這是計算機科學的完美契合”，賴斯大學計算工程的摩西教授如是說。1996 年度圖靈獎頒獎典禮上，該獎項的題詞評價Pnueli 1977年的論文“引發了對系統的動態行為推理的基本模式轉變”。這個很傑出的技術誕生後即在軟體工程界引起轟動，掀起了軟體工程中的一場革命，目前已成為開發反應式系統和並髮式系統時進行規格說明和驗證的工具，在晶片、硬體的設計上已經廣泛運用。
1981年，Pnueli 回到魏茲曼成為計算機科學系的教授。1999年，Pnueli加入美國紐約大學計算機科學系並出任教授一職。此外，和國外絕大多數教授一樣，Pnueli 並不拘泥於純學術的研究和教學。Pnueli 成立了幾家軟體公司，1971年成立Mini-Systems ，1984年成立AdCad。他還和朋友一起在美國麻薩諸塞州創辦了另一家公司：iLogixInc，Pnueli 擔任iLogixInc 公司的首席科學家。
Pnueli為人謙遜隨和，與中國的淵源甚深。他和2008年去世的我國著名邏輯和軟體學家唐稚松是至交，二人均是時態邏輯方面是業界領跑人。唐稚松教授提出了世界上第一個可執行時序邏輯語言XYZ/E。如果說Pnueli獲1996年圖靈獎的最大貢獻，是因開創性地將時序邏輯引入計算科學，那么唐稚松則是第一次將這種時序邏輯形式化理論與最新軟體技術結合起來，套用該語言將狀態轉換的控制機制引入到邏輯系統之中的人。Pnueli 赴美接受圖靈獎前夕，在寫給唐稚松的信中說：“我完全相信，由於使時態邏輯成為具有‘深遠影響’的理念，你應該分享這一榮譽（指圖靈獎）中一個很有意義的部分。”
榮譽
除了圖靈獎，Pnueli還曾獲得獎項無數，其中就包括以色列獎，這是以色列給出美國國家科學院外籍院士的成員的最高榮譽。
圖靈獎獲得者
| 2000年代 | Leslie Valiant | 2010 |
| 查爾斯·薩克爾 | 2009 |
| 芭芭拉·利斯科夫 | 2008 |
| 約翰·巴科斯 | 2007 |
| 法蘭·艾倫 | 2006 |
| 彼得·諾爾 | 2005 |
| 羅伯特·卡恩 | 2004 |
| 文頓·瑟夫 | 2004 |
| 艾倫·凱 | 2003 |
| 阿迪·薩莫爾 | 2002 |
| 羅納德·李維斯特 | 2002 |
| 倫納德·阿德曼 | 2002 |
| 奧利-約翰·達爾 | 2001 |
| 克利斯登·奈加特 | 2001 |
| 姚期智 | 2000 |
| 1990年代 | 詹姆斯·尼古拉·格雷 | 1998 |
| 道格拉斯·恩格爾巴特 | 1997 |
| 艾米爾·伯努利 | 1996 |
| 曼紐爾·布盧姆 | 1995 |
| 愛德華·費根鮑姆 | 1994 |
| 拉吉·瑞迪 | 1994 |
| 理察·斯特恩斯 | 1993 |
| 尤里斯·哈特馬尼斯 | 1993 |
| 巴特勒·拉姆潑遜 | 1992 |
| 羅賓·米爾納 | 1991 |
| 費爾南多·考巴托 | 1990 |
| 1980年代 | 威廉·卡亨 | 1989 |
| 伊凡·蘇澤蘭 | 1988 |
| 約翰·科克 | 1987 |
| 霍普克羅夫特 | 1986 |
| 羅伯特·塔揚 | 1986 |
| 理察·卡普 | 1985 |
| 尼古拉斯·沃斯 | 1984 |
| 肯·湯普遜 | 1983 |
| 丹尼斯·里奇 | 1983 |
| 史蒂芬·庫克 | 1982 |
| 埃德加·弗蘭克·科德 | 1981 |
| 東尼·霍爾 | 1980 |
| 1970年代 | 肯尼斯·艾佛森 | 1979 |
| 羅伯特·弗洛伊德 | 1978 |
| 約翰·巴科斯 | 1977 |
| 達納·斯科特 | 1976 |
| 麥可·拉賓 | 1976 |
| 艾倫·紐厄爾 | 1975 |
| 赫伯特·西蒙 | 1975 |
| 唐納德·克努特 | 1974 |
| 查爾斯·巴赫曼 | 1973 |
| 艾茲赫爾·戴克斯特拉 | 1972 |
| 約翰·麥卡錫 | 1971 |
| 詹姆斯·哈迪·威爾金森 | 1970 |
| 1960年代 | 馬文·閔斯基 | 1969 |
| 理察·衛斯里·漢明 | 1968 |
| 莫里斯·威爾克斯 | 1967 |
| 艾倫·佩利 | 1966 |
