Amir Pnueli, Distinguished Computer Scientist and Researcher, Dies

Amir Pnueli, a professor of Computer Science at New York University, died suddenly on November 2 of a brain hemorrhage. Pnueli was recognized internationally as a pioneer in the area of verification, the process of formally proving that systems, such as computer hardware and software, behave as intended by their designers.

Pnueli received the ACM A. M. Turing Award in 1996 for introducing temporal logic, a formal technique for specifying and reasoning about the behavior of systems over time, to computer science. In particular, the citation lauded his landmark 1977 paper, "The Temporal Logic of Programs," as a milestone in the area of reasoning about the dynamic behavior of systems.

Pnueli was born in Nahalal, Israel, in 1941. He received a B.Sc. degree in Mathematics from the Technion-Israel Institute of Technology and a Ph.D. in Applied Mathematics from the Weizmann Institute of Science in 1967. After a post-doctoral fellowship at Stanford University and the IBM T.J. Watson Research Center, he became a senior researcher at the Weizmann Institute. In 1973, Pnueli founded the Department of Computer Science at Tel Aviv University and became its first chair. In 1981, he returned to the Weizmann Institute as Professor of Computer Science. In 1999, he joined the Courant Institute's Department of Computer Science at NYU, and in 2006 he was appointed to a Silver Professorship. NYU issued a statement mourning his passing.

Pnueli also shared the 2007 ACM Software System Award for Statemate, a software engineering tool that allows developers to formally specify the precise desired behavior of their programs.