!!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. \\