艾米爾·伯努利，出生於1941年，在以色列理工學院取得數學學士學位，1967年在魏茨曼學院以一篇關於海洋潮汐計算的畢業論文取得套用數學博士學位，而後伯努利留校任教。
基本介紹
- 中文名：艾米爾·伯努利
- 出生地：以色列的Nahalal
- 出生日期：1941 年
- 主要成就：圖靈獎
摘要,貢獻,榮譽,圖靈獎獲得者,
摘要
又一點陣圖靈獎得主去世了，他是受人尊敬的時序邏輯領域大師艾米爾· 伯努利(AmirPnueli)。今年11月2日，這位1996年度圖靈獎得主因腦出血去世，享年68歲，只剩那些熠熠生輝的科技成就留給後人。
貢獻
在計算機出現後的最初幾十年里，計算機實質上是一個巨大的計算器，數字被錄入，計算結果被輸出。直到20世紀70年代，科學家們才意識到需要正確地驗證這些計算結果。隨著電腦變得更強大，軟體更先進，多任務和變化的數據核查變得更加困難。因此，程式設計師不得不考慮到時間推移下系統的行為。在這個契機下，時序邏輯被引入計算科學，這是計算科學發展歷史的重要轉折點。
艾米爾·伯努利
艾米爾·伯努利時序邏輯也叫時態邏輯（temporal logic)，是計算機科學裡一個很專業很重要的領域。時序邏輯被用來描述為表現和推理關於時間限定的命題的規則和符號化的任何系統，主要用於形式驗證。20 世紀60 年代Arthur Prior提出介入的基於模態邏輯的特殊的時間邏輯系統，這一理論後來被艾米爾·伯努利等邏輯學家進一步發展。
後來，Pnueli在史丹福大學和IBM Waston 研究中心從事博士後的研究工作，從這時開始，他將工作研究方向轉移到計算機科學領域。1973年，他創辦了特拉維夫大學計算機科學系，並擔任第一任院長。1977 年，Pnueli開創性地把時態邏輯引入計算機科學，他的時態邏輯是非經典邏輯中的一種，研究如何處理含有時間信息的事件的命題和謂詞。現在通常稱為時序邏輯的計算機系統，就出現在這一年，Pnueli 在子程式語言與系統驗證方面做出的傑出貢獻具有里程碑意義。
“Pnueli實現了這一邏輯，這是計算機科學的完美契合”，賴斯大學計算工程的摩西教授如是說。1996 年度圖靈獎頒獎典禮上，該獎項的題詞評價Pnueli 1977年的論文“引發了對系統的動態行為推理的基本模式轉變”。這個很傑出的技術誕生後即在軟體工程界引起轟動，掀起了軟體工程中的一場革命，目前已成為開發反應式系統和並髮式系統時進行規格說明和驗證的工具，在晶片、硬體的設計上已經廣泛運用。
榮譽
除了圖靈獎，Pnueli還曾獲得獎項無數，其中就包括以色列獎，這是以色列給出美國國家科學院外籍院士的成員的最高榮譽。
圖靈獎獲得者
2000年代 | 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 |
