Obituary: Amir Pnueli, 1941–2009#

by Krzysztof R. Apt and Lenore D. Zuck

(First published in Bulletin of EATCS 100, pp. 9-10,2010).

Amir Pnueli was born in Nahalal, Israel, on April 22, 1941 and passed away in New York City on November 2, 2009 as a result of a brain hemorrhage.

Amir founded the computer science department in Tel-Aviv University in 1973. In 1981 he joined the department of mathematical sciences at the Weizmann Institute of Science, where he spent most of his career and where he held the Estrin family chair. In recent years, Amir was a faculty member at New York University where he was a NYU Silver Professor.

Throughout his career, in spite of an impressive list of achievements, Amir remained an extremely modest and selfless researcher. His unique combination of excellence and integrity has set the tone in the large community of researchers working on specification and verification of programs and systems, program semantics and automata theory. Amir was devoid of any arrogance and those who knew him as a young promising researcher were struck how he maintained his modesty throughout his career.

Amir has been an active and extremely hard working researcher till the last moment. His sudden death left those who knew him in a state of shock and disbelief.

For his achievements Amir received the 1996 ACM Turing Award. The citation reads: “For seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification.” Amir also received, for his contributions, the 2000 Israel Award in the area of exact sciences. More recently, in 2007, he shared the ACM Software System Award. Furthermore, Amir had received the honoris causa doctorate degree from several of universities.

Temporal logic is by now a routine approach to specification and verification of concurrent, reactive, hybrid and real-time systems. The origin of this approach can be traced back to a single paper written by Amir, The Temporal Logic of Programs, 18th Annual Symposium on Foundations of Computer Science (FOCS) 1977, pp. 46-57.

At that time, the main approach to program verification was the assertional method of Tony Hoare, extended in 1976 to parallel programs by Susan Owicki and David Gries, and, independently, by Leslie Lamport. This method was applicable to parallel algorithms but using it one could prove only certain properties.

Amir recognized that an all-out verification of parallel programs called for new ideas. Temporal Logic, proposed by Amir Pnueli, is a formalism that allows for expressing relevant program properties adequately, simply, and elegantly. By suggesting proof methods that allow one to systematically establish these properties he demonstrated that temporal logic can be used in a natural way for verification of parallel programs. In his proposal he achieved a synthesis between two fields from different sciences: mathematical logic and computer science.

Amir’s early work led to Lamport’s classification of the properties of concurrent programs into the categories of safety and liveness properties (for Amir, liveness is further divided into guarantee, response, persistence, and reactivity properties). Temporal logic became a simple and intuitive specification formalism of programs and systems. This in turn led the ground for the subsequent work on model checking, an automatic approach to verification of hardware components and finite-state systems. Nowadays, hardware manufacturers commonly use tools based on temporal logic for hardware verification.

Once the temporal logic approach to program specification and verification has matured, Amir published, in the nineties, jointly with Zohar Manna, two books on this subject devoted, respectively, to program specification and verification of safety properties. Unfortunately, the book about the main novelty of temporal logic—verification of liveness properties— exists only as a draft in Amir’s computer.

Since then this approach turned out to be equally well applicable to reactive, hybrid and real-time program and systems. Amir was the instigator to these and other new areas of applications of temporal logic, and always at the forefront of the development of any such application.

In recent years Amir worked on numerous new topics, to wit translation validation, where instead of verifying a translator (e.g., a compiler) one verifies each translation, verification of infinite-state systems (e.g., systems of numerous processes with similar behavior), automation of deductive reasoning, software verification (e.g., programs with heaps), verification of distributed systems, applications of mathematical and logical methods to formal specifications, and synthesis of reactive, real-time, discrete, continuous, and hybrid systems. His recent (2006) work on synthesis of synchronous “General Reactivity 1” properties resulted in a chip, which was hanging on the wall in his NYU office.

Throughout his career Amir has been a highly prolific researcher, often engaging in a collaboration with others. The DBLP website lists 250 papers of his, written with 136 coauthors. To many of us Amir has been an inspiring collaborator and mentor, as well as a warm and always supportive friend. We shall miss him dearly.