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, in what is now 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.
He 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.
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."
Join the Discussion (0)
Become a Member or Sign In to Post a Comment