Amir Pnueli

Biographical Data

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.

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 3-volumes textbook on Temporal Logic and its application to Reactive Systems of which the first two volumes are:

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

Z. Manna & A. Pnueli: "Temporal Verification of Reactive Systems: Safety", Springer-Verlag, 1995.

The third volume is expected by the end of 1997.

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.

Membership and Editorial Responsibilities

Amir Pnueli is a member of the steering committees of the conferences CAV (Computer Aided Verification), FTRTFT (Formal Techniques for Real-Time and Fault-Tolerant Systems), and ICTL (International Conference on Temporal Logic).

He is an editor of ``Science of Computer Programming'', the ``Journal of Logic and Computations'', ``Formal Methods in System Design'', and IGPL (Journal of the Interest Group in Pure and Applied Logics).

He is a member of the Beirat for the Leibniz Center for Research in Computer Science at the Hebrew University, since its inception in 1985.

Pnueli is a member of the IFIP's WG2.2 working group on Formal Description of Programming.

He has been on the program committees of POPL, FOCS, LICS, CAV, FTRTFT, Concur, PODC, and ICALP.

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.

Email address: amir@wisdom.weizmann.ac.il