April 22, 1941, Nahalal, Israel.


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


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


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).


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

United States – 1996

For seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification.

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.