1996 阿米尔·伯努利

shiyi18

Amir Pnueli
BIRTH:
April 22, 1941, Nahalal, Israel.

DEATH:
November 2, 2009 (aged 68) New York, USA.

EDUCATION:
B.Sc. (with distinction) Mathematics (Technion, 1962); Ph.D (with distinction), Applied Mathematics (Weizmann Institute of Science, 1967), and three honorary degrees.

EXPERIENCE:
Instructor, Computer Science Department, Stanford University (1967); Summer Visitor, Watson Research Center (I.B.M) Yorktown Heights, N.Y (1968); Research Fellow, Weizmann Institute of Science (1969-1970); Visitor, AI Project, Stanford University (Summer 1970); Senior Research Fellow, Department of Applied Mathematics Weizmann Institute of Science (1970-1973); Associate Professor (and Chairman), Computer Science Division Tel Aviv University (1973-1979); Visiting Associate Professor, The Moore School of Engineering University of Pennsylvania (1976-1978); Professor, Department of Applied Mathematics, Weizmann Institute of Science (1980-2009); Visiting Professor (on leave from Weizmann) Harvard University (1982-1983); A City of Grenoble (visiting) Municipal Chair at the Verimag Laboratory, Universite Joseph Fourier, Grenoble (1994-1997); Professor, Department of Computer Science, Courant Institute, New York University (1999-2009).

HONORS AND AWARDS:
ACM Turing award (1996); honorary doctorate from the University of Uppsala, Sweden (1997); honorary doctorate from Universite Joseph Fourier, Grenoble, France (1998); elected foreign associate of the (American) National Academy of Engineering (1999); Israel Prize, category of exact sciences (2000); honorary doctorate from Carl von Ossietzky Universitaet Oldenburg, Germany (2000); elected to the Israeli Academy of Sciences (2001); elected member of the European Academy of Sciences (EAS) (2004); elected member of Academia Europaea, Informatics Section (2006); Fellow of the ACM (2007). The Weizmann Institute of Science presents a memorial lecture series in his honor.

AMIR PNUELI DL Author Profile link
United States – 1996
CITATION
For seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification.

SHORT ANNOTATED
BIBLIOGRAPHY
ACM TURING AWARD
LECTURE
RESEARCH
SUBJECTS
Amir Pnueli (pronounced: p’new-EL-ee) was born on April 22, 1941, in Nahalal, Israel. His parents, Henya and Prof. Shmuel Yeshayahu (“Shay”) Pnueli, immigrated to Israel, which was then Palestine, in 1936. They settled in Nahala, a cooperative agricultural community, where Shay Pnueli was the principal of the local school and Henya Pnueli was a teacher. In 1945, when Shay was appointed to teach in a teachers' college in the kibbutz Giva'at Hashlosha, the family relocated to Hulon. In the 1960s Prof. Shay Pnueli became one of the founders of Tel-Aviv University, and chaired the Hebrew literature department there until his death in 1965. Henya Pnueli continued teaching in Gordon school at Hulon until she died at the age of 75 in 1996.

Amir attended Kugel high school in Hulon, and then Tichon Hadash in Tel Aviv. He was active in the Ha'Tnuah H'meuchedet, an Israeli youth movement affiliated with the labour party whose focus was on collaboration between academics and labour. Although Amir showed immense promise for both the humanities (which he attributed to his father) and mathematics (which he attributed to his mother), he decided to focus on mathematics, because, as he later claimed, he did not wish to compete with his accomplished father. His brother, Prof. David Pnueli (1933-2001), was an accomplished physicist who taught fluid mechanics at the Technion, the Israel Institute of Technology.

Amir studied mathematics at the Technion during 1958-1962, graduating summa cum laude. Towards the end of his undergraduate studies he was introduced to the WEIZAC, the first computer in Israel, by Prof. Philip Rabinowitz and, according to his family, “that's where his love affair with computers started.”

He continued directly to PhD studies—highly unusual in Israel at the time where an MSc was generally required for PhD studies—in the Weizmann Institute of Science in Israel. Under the supervision of Chaim Pekeris, he wrote a dissertation on Calculation of Tides in the Ocean, also called Tides in Simple Basins[1] in 1967. In addition to being a world-renowned geophysicist, Prof. Pekeris was one of the initiators of the WEIZAC project, and Amir used it for many of the calculations in his PhD dissertation.

During 1967 and 1968 Amir was a postdoctoral fellow at Stanford University and at IBM research center in Yorktown Heights, New York. At Stanford he started a fruitful collaboration with Zohar Manna on the area now known as formal methods. His initial work was on formalizing recursive functions and functional programs. The collaboration with Prof. Manna resulted in numerous research papers and three books [7].

From 1969 to 1973 Amir was a senior researcher in the department of applied mathematics at the Weizmann Institute, where he helped Shimon Even found the graduate program.

During that time he founded, with Ido and Hagi Lochover, the company Mini Systems Ltd, which provided software for the computer-aided design systems manufacturer Scitex. The company was sold to Scitex in 1984.

Amir left the Weizmann Institute to found, and then chair, the department of computer science at Tel Aviv University, where he stayed until 1980. It was during that period that Amir got deeply involved in logics and deductive methods. During a sabbatical at the University of Pennsylvania he was introduced to the work of the philosopher Arthur Prior, who had developed “tense logic” to evaluate statements whose truthfulness changes over time. Amir was the first to realize the potential implications of applying Prior's work to computer programs. Amir’s 1977 seminal paper “The Temporal Logic of Programs” [1] revolutionized the way computer programs are analyzed. At the time, practical program verification was widely considered to be hopeless. The main methodologies considered all possible pairs of program states. Amir's paper introduced the notion of reasoning about programs as execution paths, which breathed new life into the field of program verification.

To quote Amir from his talk after receiving the Israel Prize:

“In mathematics, logic is static. It deals with connections among entities that exist in the same time frame. When one designs a dynamic computer system that has to react to ever changing conditions, … one cannot design the system based on a static view. It is necessary to characterize and describe dynamic behaviors that connect entities, events, and reactions at different time points. Temporal Logic deals therefore with a dynamic view of the world that evolves over time." (Translated from the original Hebrew)

Amir and several of his colleagues returned to the Weizmann Institute in 1980, and together they built the Department of Computer Science into one of the leading departments in the world. He was appointed to the Estrin Chair in November 2000. In 2000 Amir was awarded the Israel Prize in field of Computer Science, “for his breakthrough contribution in the verification of parallel and reactive systems by the introduction of the specification language of Temporal Logic, and the development of methods and algorithms for verifying the correctness of reactive programs and systems.” In 2001, Amir was elected to the Israeli Academy of Science.

Author: Lenore Zuck


[1] Amir himself has translated the title of his dissertation in two different ways in his curriculum vita.



阿米尔-普努埃利
出生时。
1941年4月22日，以色列纳哈勒。

逝世。
2009年11月2日（68岁），美国纽约。

学历。
理学学士（优秀），数学（Technion，1962）；博士（优秀），应用数学（Weizmann科学研究所，1967），以及三个荣誉学位。

工作经验。
斯坦福大学计算机科学系讲师（1967年）；沃森研究中心（I.B.M）Yorktown Heights, N. Y（1968年）的暑期访问学者。 1968年）；魏茨曼科学研究所研究员（1969-1970年）；斯坦福大学人工智能项目访问者（1970年夏季）；魏茨曼科学研究所应用数学系高级研究员（1970-1973年）；特拉维夫大学计算机科学部副教授（和主席）（1973-1979年）；宾夕法尼亚大学摩尔工程学院客座副教授（1976-1978年）。魏茨曼科学研究所应用数学系教授（1980-2009）；哈佛大学客座教授（从魏茨曼休假）（1982-1983）；格勒诺布尔市（访问）Verimag实验室的市级主席，约瑟夫-傅立叶大学，格勒诺布尔（1994-1997）；纽约大学库兰特研究所计算机科学系教授（1999-2009）。

荣誉和奖项。
ACM图灵奖（1996年）；瑞典乌普萨拉大学荣誉博士学位（1997年）；法国格勒诺布尔约瑟夫-傅立叶大学荣誉博士学位（1998年）；当选（美国）国家工程院外籍院士（1999年）；以色列精确科学类奖（2000年）。卡尔-冯-奥西茨基大学荣誉博士，德国奥尔登堡（2000年）；当选以色列科学院院士（2001年）；当选欧洲科学院院士（2004年）；当选欧洲科学院信息学部院士（2006年）；ACM研究员（2007年）。魏茨曼科学研究所为他举办了一个纪念性的系列讲座。

AMIR PNUELI DL作者简介链接
美国 - 1996年
获奖情况
将时态逻辑引入计算科学的开创性工作，以及对程序和系统验证的杰出贡献。

简短注释
书目
亚马逊图灵奖
讲座
研究
课题
Amir Pnueli（发音：p'new-EL-ee）于1941年4月22日出生在以色列的Nahalal。他的父母Henya和Shmuel Yeshayahu（"Shay"）Pnueli教授于1936年移民到以色列，当时是巴勒斯坦。他们在纳哈拉（Nahala）定居，这是一个合作农业社区，谢伊-普努埃利是当地学校的校长，亨亚-普努埃利是一名教师。1945年，当沙伊被任命在吉瓦特哈什洛沙集体农庄的一所师范学院任教时，他们全家迁往胡隆。20世纪60年代，谢伊-普努埃利教授成为特拉维夫大学的创始人之一，并在那里担任希伯来语文学系主任，直到1965年去世。亨利娅-普努埃利继续在胡隆的戈登学校任教，直到1996年75岁时去世。

阿米尔在胡隆的库格尔高中上学，然后在特拉维夫的蒂琼哈达什上学。他积极参加Ha'Tnuah H'meuchedet，这是一个隶属于劳工党的以色列青年运动，其重点是学术和劳工之间的合作。尽管阿米尔在人文学科（他认为是他父亲的功劳）和数学（他认为是他母亲的功劳）方面都表现出巨大的潜力，但他决定专注于数学，因为正如他后来所说，他不希望与他有成就的父亲竞争。他的哥哥大卫-普努埃利教授（1933-2001）是一位成功的物理学家，在以色列理工学院教授流体力学。

1958-1962年期间，阿米尔在以色列理工学院学习数学，以最优异的成绩毕业。在本科学习即将结束时，菲利普-拉比诺维茨教授向他介绍了以色列的第一台计算机WEIZAC，据他的家人说，"这就是他对计算机的热爱的开始。"

他继续在以色列的魏兹曼科学研究所直接攻读博士学位--在当时的以色列，攻读博士学位一般需要硕士学位，这一点很不寻常。在Chaim Pekeris的指导下，他在1967年写了一篇关于海洋中的潮汐计算的论文，也叫简单盆地的潮汐[1]。除了是世界知名的地球物理学家外，Pekeris教授还是WEIZAC项目的发起人之一，阿米尔的博士论文中的许多计算都使用了该项目。

1967年和1968年期间，阿米尔在斯坦福大学和纽约约克敦高地的IBM研究中心担任博士后研究员。在斯坦福大学，他与Zohar Manna在现在被称为形式化方法的领域开始了富有成效的合作。他最初的工作是对递归函数和函数程序进行形式化。与曼纳教授的合作产生了许多研究论文和三本书[7]。

从1969年到1973年，阿米尔是魏茨曼研究所应用数学系的高级研究员，他在那里帮助希蒙-埃文创立了研究生课程。

在此期间，他与伊多和哈吉-洛乔弗一起创建了迷你系统有限公司，该公司为计算机辅助设计系统制造商Scitex提供软件。该公司于1984年卖给了Scitex公司。

阿米尔离开魏茨曼研究所后，在特拉维夫大学创办了计算机科学系，并担任系主任，他在那里一直待到1980年。正是在这一时期，阿米尔深入研究了逻辑学和推理方法。在宾夕法尼亚大学休假期间，他被介绍给哲学家阿瑟-普莱尔的工作，他开发了 "时态逻辑 "来评估真伪随时间变化的语句。阿米尔是第一个意识到将Prior的工作应用于计算机程序的潜在意义的人。阿米尔1977年发表的开创性论文《程序的时态逻辑》[1]彻底改变了计算机程序的分析方式。当时，人们普遍认为实际的程序验证是无望的。主要的方法论考虑了所有可能的程序状态对。阿米尔的论文引入了将程序推理为执行路径的概念，这为程序验证领域注入了新的活力。

引用阿米尔在获得以色列奖后的演讲中的话说

"在数学中，逻辑是静态的。它处理的是存在于同一时间范围内的实体之间的联系。当人们设计一个必须对不断变化的条件做出反应的动态计算机系统时，......我们不能以静态的观点来设计系统。有必要对连接不同时间点的实体、事件和反应的动态行为进行定性和描述。因此，时间逻辑处理的是一个随时间演变的动态世界观"。(译自希伯来语原文)

1980年，阿米尔和他的几位同事回到了魏茨曼研究所，他们一起将计算机科学系建成了世界上领先的系之一。2000年11月，他被任命为埃斯特林主席。2000年，阿米尔被授予计算机科学领域的以色列奖，"以表彰他通过引入时态逻辑的规范语言，以及开发验证反应式程序和系统的正确性的方法和算法，在验证并行和反应式系统方面做出的突破性贡献"。2001年，阿米尔被选为以色列科学院院士。

作者简介 勒诺尔-扎克


[1] 阿米尔本人在他的履历中用两种不同的方式翻译了他的论文题目。