National Academies Press: OpenBook

Memorial Tributes: Volume 16 (2012)

Chapter: AMIR PNUELI

« Previous: MAX S. PETERS
Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×

image

Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×

AMIR PNUELI

1941–2009

Elected in 1999

“For the invention of temporal logic and other tools for designing and
verifying software and systems.”

BY DAVID HAREL AND MOSHE VARDI

AMIR PNUELI, a pioneer in the fields of specification, verification, and analysis of computer systems, and a Turing Award winner, died after suffering a brain hemorrhage on November 2, 2009. His sudden death shocked the international computing community.

A brilliant man who was shy, modest, and graceful, Pnueli, or simply Amir as he was called by anyone who knew him, was born in Nahalal, in what is now Israel, on April 22, 1941. He spent the bulk of his career at Tel Aviv University and at the Weizmann Institute of Science in Israel and in recent years also at New York University.

Amir did his doctoral work at Weizmann in applied mathematics under the late Chaim L. Pekeris, writing a thesis in 1967 on the calculation of ocean tides. Immediately thereafter he made a transition to computer science, working as a postdoctoral fellow at Stanford University and at IBM’s research center in Yorktown Heights, New York, for two years. He returned to Israel in 1968 as a faculty member in the Department of Applied Mathematics at the Weizmann Institute and in 1973 moved to Tel Aviv University, where he founded the Department of Computer Science and was its first chair. In 1980, Pnueli returned to the Weizmann Institute as a professor, together with three younger computer scientists—

Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×

Adi Shamir, Shimon Ullman, and David Harel. Together, they invigorated the computer science group there, which has grown steadily since.

Amir’s modest demeanor belied groundbreaking technical achievements. His 1977 paper, “The Temporal Logic of Programs,” marked a crucial turning point in the verification of concurrent and reactive systems. Incidentally, the paper was published in the proceedings of the Institute of Electrical and Electronics Engineers Symposium on Foundations of Computer Science but never in a journal; it apparently did not have to appear in an archival journal to become so influential. 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. His 1977 paper opened up a new world for computer scientists, and its impact is crucially felt in both the theory and the practice of the continuously growing field of program verification and analysis. At the time of its writing, program verification was widely considered a hopeless challenge, but Pnueli’s paper quietly established a framework for advanced techniques and gave new life to the domain. For this contribution, Pnueli received the Association for Computing Machinery’s A. M. Turing Award in 1996, considered the “Nobel Prize” of computing. The citation reads: “For his seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification.” Throughout the rest of his career, Pnueli continued to extend and strengthen his ideas and to contribute to the development of other verification methods. In a joint paper with David Harel in 1986, they coined the term “reactive system” to describe systems that maintain an ongoing interaction with their environment and 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 numerous additional contributions to a number of related topics, from algorithmic verification to

Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×

automated synthesis of reactive modules. Noteworthy was his extremely fruitful longtime collaboration with Zohar Manna from Stanford University, with whom he coauthored books on temporal logic and its use in the specification and verification of concurrent and reactive systems.

He had boundless curiosity and was deeply interested in developing techniques that could be used in industrial applications, not only research settings. Over the years he cofounded a number of companies, designing and supervising systems that included message switching, operating systems, software development tools, and compilers.

Pnueli’s graciousness and humility endeared him to colleagues and students alike. He listened attentively to all who sought him out, and he had a knack for finding the best in what they said. “People loved working with him because he made them feel smart,” said Lenore Zuck, a former doctoral student who is currently at the University of Illinois in Chicago. At work, Pnueli was laid-back and informal, alternating between research and conversation and indulging in long digressions about politics, food, music, and literature. “It never felt tiring to work with him,” said Zuck. Beneath his casual comportment lay deep insight and intuition, and collaborations often happened inadvertently. One could start a new piece of work in a discussion with Amir while standing in line for lunch at the cafeteria or during a coffee break at a conference in some remote part of the world.

Amir’s accomplishments were also honored in 2000 by the Israel Prize, the state’s highest honor, and in 2007 by the ACM Software System Award, given to him jointly with a team of colleagues for their work on Statemate, a software engineering tool that evolved from the Statecharts language and that supports visual graphical specifications that represent the intended functions and behavior of a system. He also received honorary doctorates from the University of Uppsala, the Université Joseph Fourier in Grenoble, and the Carl von Ossietzky Universität in Oldenburg.

At Pnueli’s funeral the first-listed author of this tribute challenged himself to identify Amir’s vices but found it very

Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×

difficult. He ended up finding two. The first: in all his letters of recommendation, about anyone at all, Amir wrote only good things. But in his defense, he really believed that everyone was very good, and this was simply part of the way he considered others, out of his unusual measure of modesty. The second problem: he was often late—late in delivering a paper on time, late with a letter of recommendation, late with a report, late with the response to some request, and so forth. But here too, in his defense, the issue was always taken care of eventually and was always done in depth and in detail and combined with the great grace of his personality and his deep wisdom.

Amir Pnueli died at the scientifically young age of 68, when he was in the process of doing some of his best work. We will never know what else he would have achieved, nor what other ideas and directions he would have brought to computer science, if he had lived another 15 or 20 years, as he so very well deserved. For us—his direct scientific beneficiaries—we followed him not just for his intelligence, his wisdom, and his universally acknowledged greatness as a scientist but also for his personality, for his ability to share with everyone his wisdom and ideas—everyone small and large—with his hallmark unlimited generosity.

Amir is survived by his wife, Ariela; his three children, Shira, Ishai, and Noga; and his grandchildren, Noam, Romy, Gaya, and Ella.

Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×

This page intentionally left blank.

Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×
Page 238
Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×
Page 239
Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×
Page 240
Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×
Page 241
Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×
Page 242
Suggested Citation:"AMIR PNUELI." National Academy of Engineering. 2012. Memorial Tributes: Volume 16. Washington, DC: The National Academies Press. doi: 10.17226/13338.
×
Page 243
Next: JOSEPH B. REAGAN »
Memorial Tributes: Volume 16 Get This Book
×
Buy Hardback | $62.00 Buy Ebook | $49.99
MyNAP members save 10% online.
Login or Register to save!
Download Free PDF

This is the 16th Volume in the series Memorial Tributes compiled by the National Academy of Engineering as a personal remembrance of the lives and outstanding achievements of its members and foreign associates. These volumes are intended to stand as an enduring record of the many contributions of engineers and engineering to the benefit of humankind. In most cases, the authors of the tributes are contemporaries or colleagues who had personal knowledge of the interests and the engineering accomplishments of the deceased. Through its members and foreign associates, the Academy carries out the responsibilities for which it was established in 1964.

Under the charter of the National Academy of Sciences, the National Academy of Engineering was formed as a parallel organization of outstanding engineers. Members are elected on the basis of significant contributions to engineering theory and practice and to the literature of engineering or on the basis of demonstrated unusual accomplishments in the pioneering of new and developing fields of technology. The National Academies share a responsibility to advise the federal government on matters of science and technology. The expertise and credibility that the National Academy of Engineering brings to that task stem directly from the abilities, interests, and achievements of our members and foreign associates, our colleagues and friends, whose special gifts we remember in this book.

  1. ×

    Welcome to OpenBook!

    You're looking at OpenBook, NAP.edu's online reading room since 1999. Based on feedback from you, our users, we've made some improvements that make it easier than ever to read thousands of publications on our website.

    Do you want to take a quick tour of the OpenBook's features?

    No Thanks Take a Tour »
  2. ×

    Show this book's table of contents, where you can jump to any chapter by name.

    « Back Next »
  3. ×

    ...or use these buttons to go back to the previous chapter or skip to the next one.

    « Back Next »
  4. ×

    Jump up to the previous page or down to the next one. Also, you can type in a page number and press Enter to go directly to that page in the book.

    « Back Next »
  5. ×

    Switch between the Original Pages, where you can read the report as it appeared in print, and Text Pages for the web version, where you can highlight and search the text.

    « Back Next »
  6. ×

    To search the entire text of this book, type in your search term here and press Enter.

    « Back Next »
  7. ×

    Share a link to this book page on your preferred social network or via email.

    « Back Next »
  8. ×

    View our suggested citation for this chapter.

    « Back Next »
  9. ×

    Ready to take your reading offline? Click here to buy this book in print or download it as a free PDF, if available.

    « Back Next »
Stay Connected!