Amir Pnueli

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