Amir Pnueli (1941-2009)

Amir Pnueli passed away Monday from a brain hemorrhage. Amir was an expert in program verification who won the 1996 Turing Award primarily for his 1977 FOCS paper The Temporal Logic of Programs. Lenore Zuck shares her thoughts.

I'm reading through what people wrote about Amir in the past 30 or so hours since we received the sad news of his passing. I'm leafing through the citations of his numerous awards and honorary degrees, the list of academies of which he was a member, and the lists of his unique accomplishments. Throughout today I was helping with NYU's press release about him. Everybody mentions how brilliant he was, how modest he was, how pleasant he was, how gracious he was. Some mention his patience with those of us who are less talented than him. What is mentioned less is how much fun he was to work with, how he put the people around him at ease, how he managed to find good ideas in seemingly random thoughts people brought to him.

I recall the hours I've spent with Amir as a graduate student: joking, our regular Friday afternoon meetings solving the acrostic puzzle of "Koteret Rashit", discussing books, news, politics, and taking work breaks. It's a wonder we got anything done. It's a wonder we got so much done. This was Amir's style -- alternating between work and play, and making large strides in research while fostering the most pleasant work environment imaginable. Years later, when we were working together at NYU, it was the same with our joint PhD students. Long sessions consisting mainly of laughter, with some breaks for coffee and sweets, at the end of which I always found myself stunned how we made so much progress during all the hilarity.

I'm trying to recall Amir's funniest lines. Some don't translate, some require too much background. But I thought of a few that may illustrate Amir's special humor. When a student of his was called to military reserve duty whenever his oral exam for the completion of his MSc was scheduled, (temporal logic) until he found a note from Amir saying "you had your oral exam in absentia and you passed with flying colors." Or when I interchanged N and M in a paper, on which, upon proof reading, Amir wrote a note "even for N=M" when I claimed I proved something for any N. Or... after long arguments with me that the past operators in temporal logic are not needed, he gave a lecture in which he basically admitted they were useful, with slides whose titles were "Admitting the Past" and "Why Should We be Ashamed of the Past" that I felt were for me. And the list goes on.

I've collaborated with Amir since I was a graduate student. I've had several joint students with him. I've worked with his students. I've held regular meetings with him, the next one is scheduled for this Friday -- I still cannot bring myself to remove it from my calendar. I cannot imagine life without him. He was a genius, a friend, a colleague, one of a kind. I feel fortunate to have had the opportunity to know him, to have worked him, to have learnt so much from him. May his memory, legacy, and example stay with us.

Lenore D. Zuck, Arlington, Virginia, November 3rd, 2009

Update 11/15: NYT Obit for Pnueli