He finished his B.Sc. degree in Mathematics at the Technion, Haifa, and received his Ph.D. degree in Applied Mathematics at the Weizmann Institute of Science, Rehovot, Israel, submitting a thesis on "Calculation of Tides in the Ocean" in 1967.
He switched into Computer Science while being a post-doctoral fellow at Stanford University, and at Watson Research Center, Yorktown.
He then returned to Israel to a position of a Senior Researcher in the Department of Applied Mathematics of the Weizmann Institute.
In 1973, Prof. Pnueli moved to Tel-Aviv University, where he founded the Department of Computer Science and was its first chairman.
In 1981, Pnueli returned to the Weizmann Institute, as a Professor of Computer Science.
In 1997, Pnueli was appointed as the head of the "Minerva Center for Verification of Reactive Systems".
In 1999, Pnueli joined the Computer Science Department of New York University.
Prof. Pnueli is the 1996 recipient of the ACM Turing award "For his seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification."
Beside his more theoretical work, concerning a complete axiom system and proof theory for program verification by temporal logic, he also contributed to algorithmic research in this area. He developed a deductive system for linear-time temporal logic and model-checking algorithms for the verification of temporal properties of finite-state systems. Together with David Harel, Pnueli worked on the semantics and implementation of Statecharts, a visual language for the specification, modeling, and prototyping of reactive systems. This language has been applied to avionics, transport, and electronic hardware systems. His current research interests involve synthesis of reactive modules, automatic verification of multi-process systems, and specification methods that combine transition systems with temporal logic.
Together with Zohar Manna, he is the author of a textbook series on Temporal Logic and its application to Reactive Systems of which the first two volumes are:
A third volume is in the planning.
In May 97, Pnueli received an honorary doctorate from the University of Uppsala, Sweden.
In December 1998, Amir Pnueli will receive an honorary doctorate from Universite Joseph Fourier, Grenoble, France.
In 1984, Mini-Systems was acquired by Scitex, and Prof. Pnueli moved on to found, together with two of his previous partners and Prof. David Harel, also from the Weizmann Institute, the company AdCad. In the years 1984-1989, Prof. Pnueli supervised and designed (together with David Harel) the first version of the Statemate system. This implementation effort required continuous research to clarify the semantics of synchronous languages, among which, Statecharts occupy a prominent position.
The company AdCad later evolved into i-Logix, a firm constructing Computer Aided Software Engineering tools for the specification and design of real time reactive embedded systems, and which is the current producer of the various versions of the Statemate systems and its later derivatives.
He is married and has 3 children and 1 grandchild.
back to homepage