NYU Professor Amir Pnueli, 68, Distinguished Computer Scientist
Amir Pnueli, on the occasion of being awarded the Israel Prize in 2000
(
Photo © Dan Porges
)
The NYU Department of Computer Science and the entire university community mourn the sudden passing of Professor Amir Pnueli, who died on November 2 of a brain hemorrhage. Professor Pnueli was an internationally recognized 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.
Professor Pnueli was the recipient of the 1996 Association for Computing Machinery Alan M. Turing Award, the highest distinction that can be bestowed on a computer scientist. He was also the recipient of the Israel Prize, the state's highest honor. He was a foreign associate of the National Academy of Engineering, a foreign member of the Academia Europaea (Informatics section), and a member of the Israel Academy of Sciences and Humanities. He received honorary doctorate degrees from the University of Uppsala, Sweden, Joseph Fourier University, Grenoble, France, and the Carl von Ossietzky University of Oldenburg, Germany, as well as numerous other professional accolades.
Amir Pnueli was born in Nahalal, Israel, on April 22, 1941. He received a B.Sc. degree in Mathematics from the Technion 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, Professor 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. He supervised more than 30 Ph.D. theses during his career in Israel and New York.
Professor Pnueli is particularly noted for introducing temporal logic, a formal technique for specifying and reasoning about the behavior of systems over time, to computer science. The 1996 Turing Award citation reads,
"Amir Pnueli made a major breakthrough in the verification and certification of concurrent and reactive systems with his landmark 1977 paper "The Temporal Logic of Programs" which was a crucial turning point in the progress of formal methods for such systems. This paper triggered a fundamental paradigm shift in reasoning about the dynamic behavior of systems; the techniques it introduces have had extraordinary influence and proved to be of lasting value. His work has been characterized as the most important contribution to program verification in the last twenty years and it has set the agenda for research and practice in the area."
Professor Pnueli was an extremely prolific and deeply creative researcher with over 250 widely-cited publications and 4 books. In recent years, he worked on compiler and translation validation, the verification of concurrent systems, and fairness of infinite behaviors, as well as the application of mathematical and logical methods to the formal specification, compositional verification, systematic development, and automatic synthesis of reactive, real-time, discrete, continuous, and hybrid systems.
Professor Pnueli always advocated applying theory to practice and was instrumental in founding two Israeli software firms. His work has influenced a wide range of scientific disciplines, including process control, databases, biological modeling, and computer hardware design as well as the avionics, transport and electronic hardware industries. He 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. The citation for the award reads:
"Statemate was the first commercial computer-aided software engineering tool to successfully overcome the challenges of complex interactive, real time computer systems, known as reactive systems. The ideas reflected in Statemate underlie many of the most powerful and widely used tools in software and systems engineering today."
Amir was a modest, kind, and warm person who was universally respected as a friend, teacher, colleague and distinguished leader. He is mourned by his colleagues and students around the world, who extend their deepest sympathy to his wife, Ariela, his three children, Noga, Shira, and Yishai, and his four beloved grandchildren.