Short Biography

Amir Pnueli was born in Nahalal, Israel, on Apr. 22, 1941.

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."

Research Activity

Prof. Pnueli is mainly known for the introduction of temporal logic into Computer Science; his work on the application of temporal logic and similar formalisms for the specification and verification of reactive systems; the identification of the class of "Reactive Systems" as systems whose formal specification, analysis, and verification require a distinctive approach; and the development of a rich and detailed methodology, based on temporal logic, for the formal treatment of reactive system; extending this methodology into the realm of real-time systems; and more recently, introducing into formal analysis the models of hybrid systems with appropriate extension of the temporal-logic based methodology.

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:

  • Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.

  • Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.

    A third volume is in the planning.

    Research interests

    Semantics and Verification of Concurrent Programs, Temporal Logic, Logics of Programs, Specification and Non Procedural languages, Automatic Proof Methods for Correctness, Verification and Synthesis of Programs, Theory of Computation, Schemata Theory and its relations to Formal Languages Theory, Automatic Recognition of Graphic Data. Specification, Verification and Systematic development of Real-Time and Hybrid Systems. Refinement, using Temporal Logic. Compositional verification of reactive, real-time, and hybrid systems. Synthesis of such systems.

    Honors and Awards

    Recipient of the ACM Turing award for 1996, "For seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification."

    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.

    Industrial Activities

    In 1971, Prof. Pnueli co-founded the software company Mini-Systems, which until 1982 was the sole software provider for Scitex, Israel, manufacturers of computer aided design systems in the color press and graphic printing areas. During this period, Pnueli designed and supervised several real time mini-computer systems, including message switching, Computer-Aided Teaching, on-line instrument testing, military real time systems, operating systems and compilers.

    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