Sign In

Communications of the ACM

News

Amir Pnueli: Ahead of His Time


1996 ACM A.M. Turing Award recipient Amir Pnueli

It is with great sadness that we note the death of Amir Pnueli, a pioneer in the fields of formal specification, verification, and analysis. Pnueli suffered a brain hemorrhage on November 2, 2009; his sudden death shocked the international computing community.

A shy and unassuming man, Pnueli was born in Nahalal, Israel, in 1941, and spent the bulk of his career at Tel Aviv University (where he founded the department of computer science), the Weizmann Institute of Science, and New York University. His modest demeanor belied groundbreaking technical achievements. In 1977, Pnueli's paper, "The Temporal Logic of Programs," marked a crucial turning point in the verification of concurrent and reactive systems. Temporal logic was developed by philosophers in the late 1950s to reason about the use of time in natural language. By introducing it to the field of formal methods, Pnueli gave researchers a set of tools that enabled them to specify and reason about the ongoing behavior of programs.

"That paper opened up a new world, both for him and for the field," says Moshe Y. Vardi, professor of computational engineering at Rice University. At the time, program verification was widely considered to be a hopeless challenge. But Pnueli's paper quietly established a framework for advanced techniques and gave new life to the domain. Throughout the rest of his career, Pnueli continued to refine his ideas and contribute to the development of other verification methods. He also coined the term "reactive system" to describe systems that maintain an ongoing interaction with their environment, and together with David Harel, a colleague at the Weizmann Institute, argued for its significance; the term has since become deeply ingrained in the literature. Working with a variety of collaborators—including current and former students—Pnueli made additional contributions to a number of related topics, from model checking to the synthesis of reactive modules. "He had boundless curiosity," says Harel.

Pnueli was deeply interested in developing techniques that could be used in industrial applications and not only research settings. He cofounded several companies, designing and supervising systems that included message switching, operating systems, and compilers. Statecharts, a visual language for the specification and design of reactive systems that he created with Harel, has subsequently been applied to areas as diverse as avionics and electronic hardware systems.

Pnueli's graciousness and humility endeared him to colleagues and students alike. He listened attentively to all who sought him out, and had a knack for finding the best in what they said. "People loved working with him because he made them feel smart," says Lenore Zuck, a former graduate student who is currently an associate professor at the University of Illinois at Chicago. At work, Pnueli was laid-back and informal, alternating between research and conversation and indulging in long digressions about politics, food, and the latest title from Am Oved, an Israeli publishing house. "It never felt tiring to work with him," says Zuck.


His graciousness and humility endeared Pnueli to colleagues and students alike.


Beneath his casual comportment lay deep insight and intuition, and collaborations, says Harel, often happened inadvertently. "We once started something while standing in line for lunch at the cafeteria," says Harel. "Another time, it was at a conference coffee break." In fact, their work on reactive systems began on a plane flight. While discussing Statecharts, the visual language he had recently created, Harel suggested it was useful for particular kinds of systems—systems that interact frequently with one another and don't do heavy computation. "And Amir said, 'Yes, I thought the same thing. Maybe we should call them reactive systems,"' recalls Harel. "I said, 'Bingo.' And then we spent the next hour talking about what we mean."

Pnueli's accomplishments were widely celebrated. In 1996, he received ACM's A.M. Turing Award for his work in temporal logic and contributions to program and system verification. These accomplishments were also honored in 2000 by the Israel Prize for Exact Sciences, the state's highest honor. More recently, Pnueli received the 2007 ACM Software System Award, with Harel and others, for their work on Statemate, a software engineering tool that evolved from the Statecharts language and supports visual, graphical specifications that represent the intended functions and behavior of a system.

At Pnueli's funeral, Harel challenged himself to identify one of his colleague's vices. The verdict: procrastination. "He was often late," recalled Harel. In Pnueli's defense, he continued, the issue was always eventually taken care of, and "in great depth, in detail, and combined with the great grace of his personality and his deep wisdom."

Back to Top

Author

Leah Hoffmann is a Brooklyn-based technology writer.

Back to Top

Footnotes

DOI: http://doi.acm.org/10.1145/1629175.1629187


©2010 ACM  0001-0782/10/0100  $10.00

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee.

The Digital Library is published by the Association for Computing Machinery. Copyright © 2010 ACM, Inc.


Comments


Dennis Shasha

When I was a graduate student at Harvard in the early 1980s,
Amir came to visit for a year.
He gave a lecture about temporal logic and I found the simplicity
of the boxes and diamonds to be appealing.
So, I sketched out a probability one proof of the Ethernet protocol
in collaboration with William Ewald (now a law professor) and brought
it to Amir.
Generously, he worked with me until the
deadline and we ended with a nice paper
that was finally published in the Principles of Programming Languages
Conference with the perhaps overwrought title:
"Temporal verification of carrier-sense local area network protocols."
Amir once said that was his first paper in distributed verification.

Amir later came to New York University,
building it into the verification powerhouse that it is.
Through all my dealings with Amir, his cheerful good nature
and straightforwardness have so nicely complemented his evident genius.
He was just a great person to know.

Dennis


Displaying 1 comment

Comment on this article

Signed comments submitted to this site are moderated and will appear if they are relevant to the topic and not abusive. Your comment will appear with your username if published. View our policy on comments

(Please sign in or create an ACM Web Account to access this feature.)

Create an Account

Log in to Submit a Signed Comment

Sign In »

Sign In

Signed comments submitted to this site are moderated and will appear if they are relevant to the topic and not abusive. Your comment will appear with your username if published. View our policy on comments
Forgot Password?

Create a Web Account

An email verification has been sent to youremail@email.com
ACM veriŞes that you are the owner of the email address you've provided by sending you a veriŞcation message. The email message will contain a link that you must click to validate this account.
NEXT STEP: CHECK YOUR EMAIL
You must click the link within the message in order to complete the process of creating your account. You may click on the link embedded in the message, or copy the link and paste it into your browser.