Amir Pnueli

Biographical Sketch

Amir Pnueli was born in Nahalal, Israel, in April 22, 1941. In 1945 he moved to Holon with his parents, Henia and Professor Shai Pnueli. His father was later one of the founders of Tel –Aviv University, and headed its Department of Hebrew Literature.
Amir studied at the Kugel High-school in Holon and the New High-school in Tel-Aviv. He later received his Bachelor's degree in Mathematics from the Technion- Israel Institute of Technology in Haifa in 1962, and his Ph.D. in applied mathematics from the Weizmann Institute of Science in 1967. His thesis, supervised by Haim Pekeris, the founder of the Applied Mathematics Department, was on the topic of "Calculation of Tides in the Ocean". He switched to computer science during his stay as a post-doctoral fellow at Stanford University and the IBM T.J. Watson Research Center in 1967-1968.

In 1969 he returned from his postdoctoral studies to Israel as a researcher at the Weizmann Institute. In 1973 he moved to Tel Aviv University where he was the founder and first chair of the Computer Science Department. In 1981 he returned to the Weizmann Institute as a professor of computer science. From 1999 until his death, Pnueli also held a position at the Courant Institute's Department of Computer Science at New York University.

Amir Pnueli’s interests in computer science spanned wide areas. He is internationally recognized mostly for his pioneering work in the area of verification, and in particular for his work on introducing temporal logic to computer science and proposing the framework of temporal logic of programs.

In their early years, computers dealt mostly with simple input-output calculations. Verifying the correctness of a program of this type was a relatively simple matter. But with time, computers became more powerful and dealt with more complex tasks, and subsequently verification grew harder. Programmers dealing with complex systems with many inputs and rich ensemble of scenarios had to take into account the behavior of the system over time as the program must respond to new data and dynamically changing external signals.

Amir Pnueli became interested in this problem and looked for mechanisms that could help providing a better understanding and convenient tools for handling it. While studying this problem, he came across the field of philosophical logic called “tense logic”, which is used to evaluate logical formulas whose truthfulness changes over time. A formula in this framework may hold at some times and be false at other times, and the mechanism enables making statements about its correctness. Amir realized that this logic is just what’s needed in order to reason about the properties of computer programs. His insights on how this logic can be used for dealing with the correctness of computer programs appeared in 1977 in a landmark paper titled “The Temporal Logic of Programs.” Some twenty years later, in 1996, Amir received the 1996 Association for Computing Machinery Alan M. Turing Award, the highest distinction that can be bestowed on a computer scientist, for this 1977 paper. The award citation reads:

“Amir Pnueli made a major breakthrough in the verification and certification of concurrent and reactive systems with his landmark 1977 paper "The Temporal Logic of Programs" which was a crucial turning point in the progress of formal methods for such systems. This paper triggered a fundamental paradigm shift in reasoning about the dynamic behavior of systems; the techniques it introduces have had extraordinary influence and proved to be of lasting value. His work has been characterized as the most important contribution to program verification in the last twenty years and it has set the agenda for research and practice in the area.”

Indeed, temporal logic is used today in many applications for specifying and verifying properties of software and hardware. For example, manufacturers of VLSI chips use software employing temporal logic to verify that the various components printed on them perform their calculations as they were intended to, and programmers use temporal logic to minimize the number of errors in their software. All of those applications follow the paradigm developed by Amir over 30 years earlier.

Amir Pnueli was an extremely prolific and deeply creative researcher. He supervised more than 30 Ph.D. theses and wrote over 250 widely-cited publications and 4 books during his career. In recent years, he worked on compiler and translation validation, the verification of concurrent systems, the paradigm of model checking, and fairness of infinite behaviors, as well as the application of mathematical and logical methods to the formal specification, compositional verification, systematic development, and automatic synthesis of reactive, real-time, discrete, continuous, and hybrid systems.

Amir also believed in applying theory to practice. He was involved in founding two Israeli startup software firms, Mini-Systems in 1971 and AdCad in 1984. He shared the 2007 ACM Software System Award for Statemate, a software engineering tool that allows developers to formally specify the precise desired behavior of their programs. The citation for the award reads:

"Statemate was the first commercial computer-aided software engineering tool to successfully overcome the challenges of complex interactive, real time computer systems, known as reactive systems. The ideas reflected in Statemate underlie many of the most powerful and widely used tools in software and systems engineering today."

Amir was also the recipient of the Israel Prize, the state's highest honor. He was a foreign associate of the National Academy of Engineering, a foreign member of the Academia Europaea (Informatics section), and a member of the Israel Academy of Sciences and Humanities. He received honorary doctorate degrees from the University of Uppsala, Sweden, Joseph Fourier University, Grenoble, France, and the Carl von Ossietzky University of Oldenburg, Germany, as well as numerous other professional accolades.

Amir was a modest, kind, and warm person who was universally respected as a friend, teacher, colleague and distinguished leader. He was married to Ariela and had two daughters, Shira and Noga, and a son, Ishay. He died on November 2, 2009, in NY, of a brain hemorrhage. The following year the Faculty of Mathematics and Computer Science of the Weizmann Institute of Science established the Pnueli Memorial Lecture, which is presented annually.