阿米尔·伯努利（Amir Pnueli，1941年4月22日 - 2009年11月2日），以色列计算机科学家，1996年图灵奖得主，以表彰其在计算科学中引入时间逻辑的开创性工作以及在程序和系统验证方面的杰出贡献。

阿米尔于1941年4月22日出生在以色列纳哈拉尔，他的父母在1936年移民到当时的巴勒斯坦以色列，定居在纳哈拉尔，父母都从事教育行业。1945年，他们全家随父亲工作变动搬到休伦。20世纪60年代，他的父亲成为特拉维夫大学创始人之一。

阿米尔从小受到良好的教育，1958年至1962年间在以色列理工学院学习数学。在本科末期，由菲利普·拉宾诺维茨教授介绍，他接触到了以色列第一台计算机 WEIZAC，据说他对计算机的热爱正是从这时开始的。

阿米尔本科毕业后直接进入以色列魏茨曼科学研究所攻读博士学位，在海姆·佩克里斯指导下，他在1967年完成了「海洋潮汐计算」的论文。佩克里斯教授不仅是世界知名的地球物理学家，还是 WEIZAC 项目的发起人之一，阿米尔的博士论文也利用该项目进行了许多计算。

1967年到1968年，阿米尔在斯坦福大学和纽约约克镇高地的 IBM 研究中心担任博士后研究员。在斯坦福，他与佐哈尔·曼纳开始了富有成效的合作，研究现在称为形式方法的领域，包括递归函数和函数式程序的形式化。

1969年至1973年，阿米尔在魏茨曼研究所应用数学系担任高级研究员。在此期间，他参与创立了 Mini Systems Ltd，为计算机辅助设计系统制造商 Scitex 提供软件，后在 1984 年被 Scitex 收购。

1973年之后，阿米尔离开魏茨曼研究所，前往特拉维夫大学创立计算机科学系并担任系主任。在那段时间，阿米尔深度投入于逻辑和演绎方法，他接触到了哲学家亚瑟·普赖尔的著作，普赖尔发展出了「时态逻辑」，用于评估那些真实性随时间变化的陈述。阿尔米是第一个意识到将普赖尔的工作应用于计算机程序潜在影响的人，1977年阿米尔发表了开创性论文「程序的时间逻辑」，彻底改变了计算机程序的分析方式。阿米尔的论文引入了将程序作为执行路径进行推理的概念，为程序验证领域注入了活力。

阿米尔还和 Zohar Manna 合著了《反应式与兵法系统的时间逻辑：规范》（1991年）和《反应式系统的时间验证：安全性》（1995年）。

1980年，阿米尔和几位同事回到了魏茨曼研究所，共同将计算机科学系建设为世界领先的系所之一「Weizmann Institute of Science」。

1999年到2009年，阿米尔在纽约大学科朗学院计算机科学系担任教授。

2000年阿米尔获得以色列最高荣誉「以色列奖」，2007年与同事共同开发的 Statemate 软件工程工具获得 ACM 软件系统奖，该工具源自 Statecharts 语言，支持代表系统预期功能和行为的可视化图形规范。

2009年11月2日，阿米尔在纽约去世，享年68岁。

参考资料

1. https://amturing.acm.org/award_winners/pnueli_4725172.cfm
2. https://www.britannica.com/biography/Amir-Pnueli
3. https://www.nae.edu/19579/19581/51314/65296/189873/AMIR-PNUELI-19412009